mathlib documentation

category_theory.opposites

Opposite categories #

We provide a category instance on Cᵒᵖ. The morphisms X ⟶ Y are defined to be the morphisms unop Y ⟶ unop X in C.

Here Cᵒᵖ is an irreducible typeclass synonym for C (it is the same one used in the algebra library).

We also provide various mechanisms for constructing opposite morphisms, functors, and natural transformations.

Unfortunately, because we do not have a definitional equality op (op X) = X, there are quite a few variations that are needed in practice.

source
theorem quiver.hom.op_inj {C : Type u₁} [quiver C] {X Y : C} :
function.injective quiver.hom.op
source
theorem quiver.hom.unop_inj {C : Type u₁} [quiver C] {X Y : Cᵒᵖ} :
function.injective quiver.hom.unop
source
@[simp]
theorem quiver.hom.unop_op {C : Type u₁} [quiver C] {X Y : C} (f : X ⟶ Y) :
f.op.unop = f
source
@[simp]
theorem quiver.hom.op_unop {C : Type u₁} [quiver C] {X Y : Cᵒᵖ} (f : X ⟶ Y) :
f.unop.op = f
source
@[protected, instance]
def category_theory.category.opposite {C : Type u₁} [category_theory.category C] :
category_theory.category Cᵒᵖ

The opposite category.

See https://stacks.math.columbia.edu/tag/001M.

Equations
source
@[simp]
theorem category_theory.op_comp {C : Type u₁} [category_theory.category C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} :
(f ≫ g).op = g.op ≫ f.op
source
@[simp]
theorem category_theory.op_id {C : Type u₁} [category_theory.category C] {X : C} :
(𝟙 X).op = 𝟙 (opposite.op X)
source
@[simp]
theorem category_theory.unop_comp {C : Type u₁} [category_theory.category C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} :
(f ≫ g).unop = g.unop ≫ f.unop
source
@[simp]
theorem category_theory.unop_id {C : Type u₁} [category_theory.category C] {X : Cᵒᵖ} :
(𝟙 X).unop = 𝟙 (opposite.unop X)
source
@[simp]
theorem category_theory.unop_id_op {C : Type u₁} [category_theory.category C] {X : C} :
(𝟙 (opposite.op X)).unop = 𝟙 X
source
@[simp]
theorem category_theory.op_id_unop {C : Type u₁} [category_theory.category C] {X : Cᵒᵖ} :
(𝟙 (opposite.unop X)).op = 𝟙 X
source
def category_theory.op_op (C : Type u₁) [category_theory.category C] :
Cᵒᵖᵒᵖ ⥤ C

The functor from the double-opposite of a category to the underlying category.

Equations
source
@[simp]
theorem category_theory.op_op_obj (C : Type u₁) [category_theory.category C] (X : Cᵒᵖᵒᵖ) :
(category_theory.op_op C).obj X = opposite.unop (opposite.unop X)
source
@[simp]
theorem category_theory.op_op_map (C : Type u₁) [category_theory.category C] (X Y : Cᵒᵖᵒᵖ) (f : X ⟶ Y) :
(category_theory.op_op C).map f = f.unop.unop
source
@[simp]
theorem category_theory.unop_unop_obj (C : Type u₁) [category_theory.category C] (X : C) :
(category_theory.unop_unop C).obj X = opposite.op (opposite.op X)
source
@[simp]
theorem category_theory.unop_unop_map (C : Type u₁) [category_theory.category C] (X Y : C) (f : X ⟶ Y) :
(category_theory.unop_unop C).map f = f.op.op
source
def category_theory.unop_unop (C : Type u₁) [category_theory.category C] :
C ⥤ Cᵒᵖᵒᵖ

The functor from a category to its double-opposite.

Equations
source
@[simp]
theorem category_theory.op_op_equivalence_counit_iso (C : Type u₁) [category_theory.category C] :
(category_theory.op_op_equivalence C).counit_iso = category_theory.iso.refl (category_theory.unop_unop C ⋙ category_theory.op_op C)
source
@[simp]
theorem category_theory.op_op_equivalence_functor (C : Type u₁) [category_theory.category C] :
(category_theory.op_op_equivalence C).functor = category_theory.op_op C
source
def category_theory.op_op_equivalence (C : Type u₁) [category_theory.category C] :
Cᵒᵖᵒᵖ ≌ C

The double opposite category is equivalent to the original.

Equations
source
@[simp]
theorem category_theory.op_op_equivalence_inverse (C : Type u₁) [category_theory.category C] :
(category_theory.op_op_equivalence C).inverse = category_theory.unop_unop C
source
@[simp]
theorem category_theory.op_op_equivalence_unit_iso (C : Type u₁) [category_theory.category C] :
(category_theory.op_op_equivalence C).unit_iso = category_theory.iso.refl (𝟭 Cᵒᵖᵒᵖ)
source
@[protected, instance]
def category_theory.is_iso_op {C : Type u₁} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.is_iso f] :
category_theory.is_iso f.op

If f is an isomorphism, so is f.op

source
theorem category_theory.is_iso_of_op {C : Type u₁} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.is_iso f.op] :
category_theory.is_iso f

If f.op is an isomorphism f must be too. (This cannot be an instance as it would immediately loop!)

source
theorem category_theory.is_iso_op_iff {C : Type u₁} [category_theory.category C] {X Y : C} (f : X ⟶ Y) :
category_theory.is_iso f.op ↔ category_theory.is_iso f
source
theorem category_theory.is_iso_unop_iff {C : Type u₁} [category_theory.category C] {X Y : Cᵒᵖ} (f : X ⟶ Y) :
category_theory.is_iso f.unop ↔ category_theory.is_iso f
source
@[protected, instance]
def category_theory.is_iso_unop {C : Type u₁} [category_theory.category C] {X Y : Cᵒᵖ} (f : X ⟶ Y) [category_theory.is_iso f] :
category_theory.is_iso f.unop
source
@[simp]
theorem category_theory.op_inv {C : Type u₁} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.is_iso f] :
(category_theory.inv f).op = category_theory.inv f.op
source
@[simp]
theorem category_theory.unop_inv {C : Type u₁} [category_theory.category C] {X Y : Cᵒᵖ} (f : X ⟶ Y) [category_theory.is_iso f] :
(category_theory.inv f).unop = category_theory.inv f.unop
source
@[simp]
theorem category_theory.functor.op_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (X Y : Cᵒᵖ) (f : X ⟶ Y) :
F.op.map f = (F.map f.unop).op
source
@[protected]
def category_theory.functor.op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :
Cᵒᵖ ⥤ Dᵒᵖ

The opposite of a functor, i.e. considering a functor F : C ⥤ D as a functor Cᵒᵖ ⥤ Dᵒᵖ. In informal mathematics no distinction is made between these.

Equations
source
@[simp]
theorem category_theory.functor.op_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (X : Cᵒᵖ) :
F.op.obj X = opposite.op (F.obj (opposite.unop X))
source
@[protected]
def category_theory.functor.unop {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ Dᵒᵖ) :
C ⥤ D

Given a functor F : Cᵒᵖ ⥤ Dᵒᵖ we can take the "unopposite" functor F : C ⥤ D. In informal mathematics no distinction is made between these.

Equations
source
@[simp]
theorem category_theory.functor.unop_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ Dᵒᵖ) (X Y : C) (f : X ⟶ Y) :
F.unop.map f = (F.map f.op).unop
source
@[simp]
theorem category_theory.functor.unop_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ Dᵒᵖ) (X : C) :
F.unop.obj X = opposite.unop (F.obj (opposite.op X))
source
@[simp]
theorem category_theory.functor.op_unop_iso_inv_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (X : C) :
F.op_unop_iso.inv.app X = 𝟙 (F.obj X)
source
def category_theory.functor.op_unop_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :
F.op.unop ≅ F

The isomorphism between F.op.unop and F.

Equations
source
@[simp]
theorem category_theory.functor.op_unop_iso_hom_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (X : C) :
F.op_unop_iso.hom.app X = 𝟙 (F.obj X)
source
def category_theory.functor.unop_op_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ Dᵒᵖ) :
F.unop.op ≅ F

The isomorphism between F.unop.op and F.

Equations
source
@[simp]
theorem category_theory.functor.unop_op_iso_hom_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ Dᵒᵖ) (X : Cᵒᵖ) :
F.unop_op_iso.hom.app X = 𝟙 (F.obj X)
source
@[simp]
theorem category_theory.functor.unop_op_iso_inv_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ Dᵒᵖ) (X : Cᵒᵖ) :
F.unop_op_iso.inv.app X = 𝟙 (F.obj X)
source
def category_theory.functor.op_hom (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
(C ⥤ D)ᵒᵖ ⥤ Cᵒᵖ ⥤ Dᵒᵖ

Taking the opposite of a functor is functorial.

Equations
source
@[simp]
theorem category_theory.functor.op_hom_map_app (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (F G : (C ⥤ D)ᵒᵖ) (α : F ⟶ G) (X : Cᵒᵖ) :
((category_theory.functor.op_hom C D).map α).app X = (α.unop.app (opposite.unop X)).op
source
@[simp]
theorem category_theory.functor.op_hom_obj (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (F : (C ⥤ D)ᵒᵖ) :
(category_theory.functor.op_hom C D).obj F = (opposite.unop F).op
source
@[simp]
theorem category_theory.functor.op_inv_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (F G : Cᵒᵖ ⥤ Dᵒᵖ) (α : F ⟶ G) :
(category_theory.functor.op_inv C D).map α = quiver.hom.op {app := λ (X : C), (α.app (opposite.op X)).unop, naturality' := _}
source
@[simp]
theorem category_theory.functor.op_inv_obj (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (F : Cᵒᵖ ⥤ Dᵒᵖ) :
(category_theory.functor.op_inv C D).obj F = opposite.op F.unop
source
def category_theory.functor.op_inv (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
(Cᵒᵖ ⥤ Dᵒᵖ) ⥤ (C ⥤ D)ᵒᵖ

Take the "unopposite" of a functor is functorial.

Equations
source
@[simp]
theorem category_theory.functor.left_op_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ Dᵒᵖ) (X Y : Cᵒᵖ) (f : X ⟶ Y) :
F.left_op.map f = (F.map f.unop).unop
source
@[protected]
def category_theory.functor.left_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ Dᵒᵖ) :
Cᵒᵖ ⥤ D

Another variant of the opposite of functor, turning a functor C ⥤ Dᵒᵖ into a functor Cᵒᵖ ⥤ D. In informal mathematics no distinction is made.

Equations
source
@[simp]
theorem category_theory.functor.left_op_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ Dᵒᵖ) (X : Cᵒᵖ) :
F.left_op.obj X = opposite.unop (F.obj (opposite.unop X))
source
@[protected]
def category_theory.functor.right_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ D) :
C ⥤ Dᵒᵖ

Another variant of the opposite of functor, turning a functor Cᵒᵖ ⥤ D into a functor C ⥤ Dᵒᵖ. In informal mathematics no distinction is made.

Equations
source
@[simp]
theorem category_theory.functor.right_op_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ D) (X Y : C) (f : X ⟶ Y) :
F.right_op.map f = (F.map f.op).op
source
@[simp]
theorem category_theory.functor.right_op_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ D) (X : C) :
F.right_op.obj X = opposite.op (F.obj (opposite.op X))
source
@[protected, instance]
def category_theory.functor.op.category_theory.full {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C ⥤ D} [category_theory.full F] :
category_theory.full F.op
Equations
source
@[protected, instance]
def category_theory.functor.op.category_theory.faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C ⥤ D} [category_theory.faithful F] :
category_theory.faithful F.op
source
@[protected, instance]
def category_theory.functor.right_op_faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : Cᵒᵖ ⥤ D} [category_theory.faithful F] :
category_theory.faithful F.right_op

If F is faithful then the right_op of F is also faithful.

source
@[protected, instance]
def category_theory.functor.left_op_faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C ⥤ Dᵒᵖ} [category_theory.faithful F] :
category_theory.faithful F.left_op

If F is faithful then the left_op of F is also faithful.

source
@[simp]
theorem category_theory.functor.left_op_right_op_iso_inv_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ Dᵒᵖ) (X : C) :
F.left_op_right_op_iso.inv.app X = 𝟙 (F.obj X)
source
def category_theory.functor.left_op_right_op_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ Dᵒᵖ) :
F.left_op.right_op ≅ F

The isomorphism between F.left_op.right_op and F.

Equations
source
@[simp]
theorem category_theory.functor.left_op_right_op_iso_hom_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ Dᵒᵖ) (X : C) :
F.left_op_right_op_iso.hom.app X = 𝟙 (F.obj X)
source
@[simp]
theorem category_theory.functor.right_op_left_op_iso_hom_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ D) (X : Cᵒᵖ) :
F.right_op_left_op_iso.hom.app X = 𝟙 (F.obj X)
source
@[simp]
theorem category_theory.functor.right_op_left_op_iso_inv_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ D) (X : Cᵒᵖ) :
F.right_op_left_op_iso.inv.app X = 𝟙 (F.obj X)
source
def category_theory.functor.right_op_left_op_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ D) :
F.right_op.left_op ≅ F

The isomorphism between F.right_op.left_op and F.

Equations
source
@[simp]
theorem category_theory.nat_trans.op_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ⟶ G) (X : Cᵒᵖ) :
(category_theory.nat_trans.op α).app X = (α.app (opposite.unop X)).op
source
@[protected]
def category_theory.nat_trans.op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ⟶ G) :
G.op ⟶ F.op

The opposite of a natural transformation.

Equations
source
@[simp]
theorem category_theory.nat_trans.op_id {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :
category_theory.nat_trans.op (𝟙 F) = 𝟙 F.op
source
@[protected]
def category_theory.nat_trans.unop {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ⟶ G) :
G.unop ⟶ F.unop

The "unopposite" of a natural transformation.

Equations
source
@[simp]
theorem category_theory.nat_trans.unop_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ⟶ G) (X : C) :
(category_theory.nat_trans.unop α).app X = (α.app (opposite.op X)).unop
source
@[simp]
theorem category_theory.nat_trans.unop_id {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ Dᵒᵖ) :
category_theory.nat_trans.unop (𝟙 F) = 𝟙 F.unop
source
@[protected]
def category_theory.nat_trans.remove_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F.op ⟶ G.op) :
G ⟶ F

Given a natural transformation α : F.op ⟶ G.op, we can take the "unopposite" of each component obtaining a natural transformation G ⟶ F.

Equations
source
@[simp]
theorem category_theory.nat_trans.remove_op_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F.op ⟶ G.op) (X : C) :
(category_theory.nat_trans.remove_op α).app X = (α.app (opposite.op X)).unop
source
@[simp]
theorem category_theory.nat_trans.remove_op_id {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :
category_theory.nat_trans.remove_op (𝟙 F.op) = 𝟙 F
source
@[simp]
theorem category_theory.nat_trans.remove_unop_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F.unop ⟶ G.unop) (X : Cᵒᵖ) :
(category_theory.nat_trans.remove_unop α).app X = (α.app (opposite.unop X)).op
source
@[protected]
def category_theory.nat_trans.remove_unop {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F.unop ⟶ G.unop) :
G ⟶ F

Given a natural transformation α : F.unop ⟶ G.unop, we can take the opposite of each component obtaining a natural transformation G ⟶ F.

Equations
source
@[simp]
theorem category_theory.nat_trans.remove_unop_id {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ Dᵒᵖ) :
category_theory.nat_trans.remove_unop (𝟙 F.unop) = 𝟙 F
source
@[simp]
theorem category_theory.nat_trans.left_op_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ Dᵒᵖ} (α : F ⟶ G) (X : Cᵒᵖ) :
(category_theory.nat_trans.left_op α).app X = (α.app (opposite.unop X)).unop
source
@[protected]
def category_theory.nat_trans.left_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ Dᵒᵖ} (α : F ⟶ G) :
G.left_op ⟶ F.left_op

Given a natural transformation α : F ⟶ G, for F G : C ⥤ Dᵒᵖ, taking unop of each component gives a natural transformation G.left_op ⟶ F.left_op.

Equations
source
@[simp]
theorem category_theory.nat_trans.left_op_id {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C ⥤ Dᵒᵖ} :
category_theory.nat_trans.left_op (𝟙 F) = 𝟙 F.left_op
source
@[simp]
theorem category_theory.nat_trans.left_op_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G H : C ⥤ Dᵒᵖ} (α : F ⟶ G) (β : G ⟶ H) :
category_theory.nat_trans.left_op (α ≫ β) = category_theory.nat_trans.left_op β ≫ category_theory.nat_trans.left_op α
source
@[simp]
theorem category_theory.nat_trans.remove_left_op_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ Dᵒᵖ} (α : F.left_op ⟶ G.left_op) (X : C) :
(category_theory.nat_trans.remove_left_op α).app X = (α.app (opposite.op X)).op
source
@[protected]
def category_theory.nat_trans.remove_left_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ Dᵒᵖ} (α : F.left_op ⟶ G.left_op) :
G ⟶ F

Given a natural transformation α : F.left_op ⟶ G.left_op, for F G : C ⥤ Dᵒᵖ, taking op of each component gives a natural transformation G ⟶ F.

Equations
source
@[simp]
theorem category_theory.nat_trans.remove_left_op_id {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C ⥤ Dᵒᵖ} :
category_theory.nat_trans.remove_left_op (𝟙 F.left_op) = 𝟙 F
source
@[simp]
theorem category_theory.nat_trans.right_op_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : Cᵒᵖ ⥤ D} (α : F ⟶ G) (X : C) :
(category_theory.nat_trans.right_op α).app X = (α.app (opposite.op X)).op
source
@[protected]
def category_theory.nat_trans.right_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : Cᵒᵖ ⥤ D} (α : F ⟶ G) :
G.right_op ⟶ F.right_op

Given a natural transformation α : F ⟶ G, for F G : Cᵒᵖ ⥤ D, taking op of each component gives a natural transformation G.right_op ⟶ F.right_op.

Equations
source
@[simp]
theorem category_theory.nat_trans.right_op_id {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : Cᵒᵖ ⥤ D} :
category_theory.nat_trans.right_op (𝟙 F) = 𝟙 F.right_op
source
@[simp]
theorem category_theory.nat_trans.right_op_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G H : Cᵒᵖ ⥤ D} (α : F ⟶ G) (β : G ⟶ H) :
category_theory.nat_trans.right_op (α ≫ β) = category_theory.nat_trans.right_op β ≫ category_theory.nat_trans.right_op α
source
@[protected]
def category_theory.nat_trans.remove_right_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : Cᵒᵖ ⥤ D} (α : F.right_op ⟶ G.right_op) :
G ⟶ F

Given a natural transformation α : F.right_op ⟶ G.right_op, for F G : Cᵒᵖ ⥤ D, taking unop of each component gives a natural transformation G ⟶ F.

Equations
source
@[simp]
theorem category_theory.nat_trans.remove_right_op_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : Cᵒᵖ ⥤ D} (α : F.right_op ⟶ G.right_op) (X : Cᵒᵖ) :
(category_theory.nat_trans.remove_right_op α).app X = (α.app (opposite.unop X)).unop
source
@[simp]
theorem category_theory.nat_trans.remove_right_op_id {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : Cᵒᵖ ⥤ D} :
category_theory.nat_trans.remove_right_op (𝟙 F.right_op) = 𝟙 F
source
@[simp]
theorem category_theory.iso.op_hom {C : Type u₁} [category_theory.category C] {X Y : C} (α : X ≅ Y) :
α.op.hom = α.hom.op
source
@[protected]
def category_theory.iso.op {C : Type u₁} [category_theory.category C] {X Y : C} (α : X ≅ Y) :
opposite.op Y ≅ opposite.op X

The opposite isomorphism.

Equations
source
@[simp]
theorem category_theory.iso.op_inv {C : Type u₁} [category_theory.category C] {X Y : C} (α : X ≅ Y) :
α.op.inv = α.inv.op
source
@[simp]
theorem category_theory.iso.unop_inv {C : Type u₁} [category_theory.category C] {X Y : Cᵒᵖ} (f : X ≅ Y) :
f.unop.inv = f.inv.unop
source
@[simp]
theorem category_theory.iso.unop_hom {C : Type u₁} [category_theory.category C] {X Y : Cᵒᵖ} (f : X ≅ Y) :
f.unop.hom = f.hom.unop
source
def category_theory.iso.unop {C : Type u₁} [category_theory.category C] {X Y : Cᵒᵖ} (f : X ≅ Y) :
opposite.unop Y ≅ opposite.unop X

The isomorphism obtained from an isomorphism in the opposite category.

Equations
source
@[simp]
theorem category_theory.iso.unop_op {C : Type u₁} [category_theory.category C] {X Y : Cᵒᵖ} (f : X ≅ Y) :
f.unop.op = f
source
@[simp]
theorem category_theory.iso.op_unop {C : Type u₁} [category_theory.category C] {X Y : C} (f : X ≅ Y) :
f.op.unop = f
source
@[simp]
theorem category_theory.nat_iso.op_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ≅ G) :
(category_theory.nat_iso.op α).inv = category_theory.nat_trans.op α.inv
source
@[protected]
def category_theory.nat_iso.op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ≅ G) :
G.op ≅ F.op

The natural isomorphism between opposite functors G.op ≅ F.op induced by a natural isomorphism between the original functors F ≅ G.

Equations
source
@[simp]
theorem category_theory.nat_iso.op_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ≅ G) :
(category_theory.nat_iso.op α).hom = category_theory.nat_trans.op α.hom
source
@[simp]
theorem category_theory.nat_iso.remove_op_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F.op ≅ G.op) :
(category_theory.nat_iso.remove_op α).inv = category_theory.nat_trans.remove_op α.inv
source
@[simp]
theorem category_theory.nat_iso.remove_op_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F.op ≅ G.op) :
(category_theory.nat_iso.remove_op α).hom = category_theory.nat_trans.remove_op α.hom
source
@[protected]
def category_theory.nat_iso.remove_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F.op ≅ G.op) :
G ≅ F

The natural isomorphism between functors G ≅ F induced by a natural isomorphism between the opposite functors F.op ≅ G.op.

Equations
source
@[simp]
theorem category_theory.nat_iso.unop_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ≅ G) :
(category_theory.nat_iso.unop α).hom = category_theory.nat_trans.unop α.hom
source
@[simp]
theorem category_theory.nat_iso.unop_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ≅ G) :
(category_theory.nat_iso.unop α).inv = category_theory.nat_trans.unop α.inv
source
@[protected]
def category_theory.nat_iso.unop {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ≅ G) :
G.unop ≅ F.unop

The natural isomorphism between functors G.unop ≅ F.unop induced by a natural isomorphism between the original functors F ≅ G.

Equations
source
@[simp]
theorem category_theory.equivalence.op_counit_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :
e.op.counit_iso = (category_theory.nat_iso.op e.counit_iso).symm
source
@[simp]
theorem category_theory.equivalence.op_inverse {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :
e.op.inverse = e.inverse.op
source
@[simp]
theorem category_theory.equivalence.op_functor {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :
e.op.functor = e.functor.op
source
@[simp]
theorem category_theory.equivalence.op_unit_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :
e.op.unit_iso = (category_theory.nat_iso.op e.unit_iso).symm
source
def category_theory.equivalence.op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :
Cᵒᵖ ≌ Dᵒᵖ

An equivalence between categories gives an equivalence between the opposite categories.

Equations
source
@[simp]
theorem category_theory.equivalence.unop_inverse {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : Cᵒᵖ ≌ Dᵒᵖ) :
e.unop.inverse = e.inverse.unop
source
@[simp]
theorem category_theory.equivalence.unop_functor {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : Cᵒᵖ ≌ Dᵒᵖ) :
e.unop.functor = e.functor.unop
source
def category_theory.equivalence.unop {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : Cᵒᵖ ≌ Dᵒᵖ) :
C ≌ D

An equivalence between opposite categories gives an equivalence between the original categories.

Equations
source
@[simp]
theorem category_theory.equivalence.unop_counit_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : Cᵒᵖ ≌ Dᵒᵖ) :
e.unop.counit_iso = (category_theory.nat_iso.unop e.counit_iso).symm
source
@[simp]
theorem category_theory.equivalence.unop_unit_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : Cᵒᵖ ≌ Dᵒᵖ) :
e.unop.unit_iso = (category_theory.nat_iso.unop e.unit_iso).symm
source
def category_theory.op_equiv {C : Type u₁} [category_theory.category C] (A B : Cᵒᵖ) :
(A ⟶ B) ≃ (opposite.unop B ⟶ opposite.unop A)

The equivalence between arrows of the form A ⟶ B and B.unop ⟶ A.unop. Useful for building adjunctions. Note that this (definitionally) gives variants

def op_equiv' (A : C) (B : Cᵒᵖ) : (opposite.op A ⟶ B) ≃ (B.unop ⟶ A) :=
op_equiv _ _

def op_equiv'' (A : Cᵒᵖ) (B : C) : (A ⟶ opposite.op B) ≃ (B ⟶ A.unop) :=
op_equiv _ _

def op_equiv''' (A B : C) : (opposite.op A ⟶ opposite.op B) ≃ (B ⟶ A) :=
op_equiv _ _
```
Equations
source
@[simp]
theorem category_theory.op_equiv_symm_apply {C : Type u₁} [category_theory.category C] (A B : Cᵒᵖ) (g : opposite.unop B ⟶ opposite.unop A) :
⇑((category_theory.op_equiv A B).symm) g = g.op
source
@[simp]
theorem category_theory.op_equiv_apply {C : Type u₁} [category_theory.category C] (A B : Cᵒᵖ) (f : A ⟶ B) :
⇑(category_theory.op_equiv A B) f = f.unop
source
@[protected, instance]
def category_theory.subsingleton_of_unop {C : Type u₁} [category_theory.category C] (A B : Cᵒᵖ) [subsingleton (opposite.unop B ⟶ opposite.unop A)] :
subsingleton (A ⟶ B)
source
@[protected, instance]
def category_theory.decidable_eq_of_unop {C : Type u₁} [category_theory.category C] (A B : Cᵒᵖ) [decidable_eq (opposite.unop B ⟶ opposite.unop A)] :
decidable_eq (A ⟶ B)
Equations
source
@[simp]
theorem category_theory.functor.op_unop_equiv_functor (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
(category_theory.functor.op_unop_equiv C D).functor = category_theory.functor.op_hom C D
source
def category_theory.functor.op_unop_equiv (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
(C ⥤ D)ᵒᵖ ≌ Cᵒᵖ ⥤ Dᵒᵖ

The equivalence of functor categories induced by op and unop.

Equations
source
@[simp]
theorem category_theory.functor.op_unop_equiv_inverse (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
(category_theory.functor.op_unop_equiv C D).inverse = category_theory.functor.op_inv C D
source
@[simp]
theorem category_theory.functor.op_unop_equiv_counit_iso (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
(category_theory.functor.op_unop_equiv C D).counit_iso = category_theory.nat_iso.of_components (λ (F : Cᵒᵖ ⥤ Dᵒᵖ), F.unop_op_iso) _
source
@[simp]
theorem category_theory.functor.op_unop_equiv_unit_iso (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
(category_theory.functor.op_unop_equiv C D).unit_iso = category_theory.nat_iso.of_components (λ (F : (C ⥤ D)ᵒᵖ), (opposite.unop F).op_unop_iso.op) _
source
@[simp]
theorem category_theory.functor.left_op_right_op_equiv_unit_iso (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
(category_theory.functor.left_op_right_op_equiv C D).unit_iso = category_theory.nat_iso.of_components (λ (F : (Cᵒᵖ ⥤ D)ᵒᵖ), (opposite.unop F).right_op_left_op_iso.op) _
source
def category_theory.functor.left_op_right_op_equiv (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
(Cᵒᵖ ⥤ D)ᵒᵖ ≌ C ⥤ Dᵒᵖ

The equivalence of functor categories induced by left_op and right_op.

Equations
source
@[simp]
theorem category_theory.functor.left_op_right_op_equiv_inverse_obj (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (F : C ⥤ Dᵒᵖ) :
(category_theory.functor.left_op_right_op_equiv C D).inverse.obj F = opposite.op F.left_op
source
@[simp]
theorem category_theory.functor.left_op_right_op_equiv_functor_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (F G : (Cᵒᵖ ⥤ D)ᵒᵖ) (η : F ⟶ G) :
(category_theory.functor.left_op_right_op_equiv C D).functor.map η = category_theory.nat_trans.right_op η.unop
source
@[simp]
theorem category_theory.functor.left_op_right_op_equiv_counit_iso (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
(category_theory.functor.left_op_right_op_equiv C D).counit_iso = category_theory.nat_iso.of_components (λ (F : C ⥤ Dᵒᵖ), F.left_op_right_op_iso) _
source
@[simp]
theorem category_theory.functor.left_op_right_op_equiv_inverse_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (F G : C ⥤ Dᵒᵖ) (η : F ⟶ G) :
(category_theory.functor.left_op_right_op_equiv C D).inverse.map η = (category_theory.nat_trans.left_op η).op
source
@[simp]
theorem category_theory.functor.left_op_right_op_equiv_functor_obj (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (F : (Cᵒᵖ ⥤ D)ᵒᵖ) :
(category_theory.functor.left_op_right_op_equiv C D).functor.obj F = (opposite.unop F).right_op