# 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.

theorem Quiver.Hom.op_inj {C : Type u₁} [] {X : C} {Y : C} :
Function.Injective Quiver.Hom.op
theorem Quiver.Hom.unop_inj {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} :
Function.Injective Quiver.Hom.unop
@[simp]
theorem Quiver.Hom.unop_op {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
f.op.unop = f
@[simp]
theorem Quiver.Hom.unop_op' {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {x : } :
@[simp]
theorem Quiver.Hom.op_unop {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
f.unop.op = f
@[simp]
theorem Quiver.Hom.unop_mk {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
instance CategoryTheory.Category.opposite {C : Type u₁} [] :

The opposite category.

Equations
• CategoryTheory.Category.opposite =
theorem CategoryTheory.op_comp_assoc {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : X Y} {g : Y Z✝} {Z : Cᵒᵖ} (h : Z) :
@[simp]
theorem CategoryTheory.op_comp {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : X Y} {g : Y Z} :
.op =
@[simp]
theorem CategoryTheory.op_id {C : Type u₁} [] {X : C} :
theorem CategoryTheory.unop_comp_assoc {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X Y} {g : Y Z✝} {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.unop_comp {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X Y} {g : Y Z} :
@[simp]
theorem CategoryTheory.unop_id {C : Type u₁} [] {X : Cᵒᵖ} :
@[simp]
theorem CategoryTheory.unop_id_op {C : Type u₁} [] {X : C} :
@[simp]
theorem CategoryTheory.op_id_unop {C : Type u₁} [] {X : Cᵒᵖ} :
@[simp]
theorem CategoryTheory.unopUnop_map (C : Type u₁) [] :
∀ {X Y : Cᵒᵖᵒᵖ} (f : X Y), .map f = f.unop.unop
@[simp]
theorem CategoryTheory.unopUnop_obj (C : Type u₁) [] (X : Cᵒᵖᵒᵖ) :
.obj X =
def CategoryTheory.unopUnop (C : Type u₁) [] :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.opOp_map (C : Type u₁) [] :
∀ {X Y : C} (f : X Y), .map f = f.op.op
@[simp]
theorem CategoryTheory.opOp_obj (C : Type u₁) [] (X : C) :
.obj X =
def CategoryTheory.opOp (C : Type u₁) [] :

The functor from a category to its double-opposite.

Equations
• = { obj := fun (X : C) => , map := fun {X Y : C} (f : X Y) => f.op.op, map_id := , map_comp := }
Instances For
@[simp]
@[simp]
theorem CategoryTheory.opOpEquivalence_counitIso (C : Type u₁) [] :
.counitIso =
@[simp]
theorem CategoryTheory.opOpEquivalence_functor (C : Type u₁) [] :
.functor =
@[simp]
theorem CategoryTheory.opOpEquivalence_inverse (C : Type u₁) [] :
.inverse =

The double opposite category is equivalent to the original.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.isIso_op {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

If f is an isomorphism, so is f.op

Equations
• =
theorem CategoryTheory.isIso_of_op {C : Type u₁} [] {X : C} {Y : C} (f : X Y) [] :

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

theorem CategoryTheory.isIso_op_iff {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.isIso_unop_iff {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
instance CategoryTheory.isIso_unop {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
Equations
• =
@[simp]
theorem CategoryTheory.op_inv {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
.op =
@[simp]
theorem CategoryTheory.unop_inv {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
.unop = CategoryTheory.inv f.unop
@[simp]
theorem CategoryTheory.Functor.op_map {C : Type u₁} [] {D : Type u₂} [] (F : ) :
∀ {X Y : Cᵒᵖ} (f : X Y), F.op.map f = (F.map f.unop).op
@[simp]
theorem CategoryTheory.Functor.op_obj {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : Cᵒᵖ) :
F.op.obj X = Opposite.op (F.obj ())
def CategoryTheory.Functor.op {C : Type u₁} [] {D : Type u₂} [] (F : ) :

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
• F.op = { obj := fun (X : Cᵒᵖ) => Opposite.op (F.obj ()), map := fun {X Y : Cᵒᵖ} (f : X Y) => (F.map f.unop).op, map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.Functor.unop_map {C : Type u₁} [] {D : Type u₂} [] (F : ) :
∀ {X Y : C} (f : X Y), F.unop.map f = (F.map f.op).unop
@[simp]
theorem CategoryTheory.Functor.unop_obj {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
F.unop.obj X = Opposite.unop (F.obj ())
def CategoryTheory.Functor.unop {C : Type u₁} [] {D : Type u₂} [] (F : ) :

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
• F.unop = { obj := fun (X : C) => Opposite.unop (F.obj ()), map := fun {X Y : C} (f : X Y) => (F.map f.op).unop, map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.Functor.opUnopIso_inv_app {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
F.opUnopIso.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
@[simp]
theorem CategoryTheory.Functor.opUnopIso_hom_app {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
F.opUnopIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
def CategoryTheory.Functor.opUnopIso {C : Type u₁} [] {D : Type u₂} [] (F : ) :
F.op.unop F

The isomorphism between F.op.unop and F.

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.unopOpIso_hom_app {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : Cᵒᵖ) :
F.unopOpIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
@[simp]
theorem CategoryTheory.Functor.unopOpIso_inv_app {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : Cᵒᵖ) :
F.unopOpIso.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
def CategoryTheory.Functor.unopOpIso {C : Type u₁} [] {D : Type u₂} [] (F : ) :
F.unop.op F

The isomorphism between F.unop.op and F.

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.opHom_obj (C : Type u₁) [] (D : Type u₂) [] (F : ()ᵒᵖ) :
.obj F = ().op
@[simp]
theorem CategoryTheory.Functor.opHom_map_app (C : Type u₁) [] (D : Type u₂) [] :
∀ {X Y : ()ᵒᵖ} (α : X Y) (X_1 : Cᵒᵖ), (.map α).app X_1 = (α.unop.app ()).op
def CategoryTheory.Functor.opHom (C : Type u₁) [] (D : Type u₂) [] :

Taking the opposite of a functor is functorial.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Functor.opInv_map (C : Type u₁) [] (D : Type u₂) [] :
∀ {X Y : } (α : X Y), .map α = Quiver.Hom.op { app := fun (X_1 : C) => (α.app (Opposite.op X_1)).unop, naturality := }
@[simp]
theorem CategoryTheory.Functor.opInv_obj (C : Type u₁) [] (D : Type u₂) [] (F : ) :
.obj F = Opposite.op F.unop
def CategoryTheory.Functor.opInv (C : Type u₁) [] (D : Type u₂) [] :

Take the "unopposite" of a functor is functorial.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Functor.leftOp_obj {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : Cᵒᵖ) :
F.leftOp.obj X = Opposite.unop (F.obj ())
@[simp]
theorem CategoryTheory.Functor.leftOp_map {C : Type u₁} [] {D : Type u₂} [] (F : ) :
∀ {X Y : Cᵒᵖ} (f : X Y), F.leftOp.map f = (F.map f.unop).unop
def CategoryTheory.Functor.leftOp {C : Type u₁} [] {D : Type u₂} [] (F : ) :

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
• F.leftOp = { obj := fun (X : Cᵒᵖ) => Opposite.unop (F.obj ()), map := fun {X Y : Cᵒᵖ} (f : X Y) => (F.map f.unop).unop, map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.Functor.rightOp_map {C : Type u₁} [] {D : Type u₂} [] (F : ) :
∀ {X Y : C} (f : X Y), F.rightOp.map f = (F.map f.op).op
@[simp]
theorem CategoryTheory.Functor.rightOp_obj {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
F.rightOp.obj X = Opposite.op (F.obj ())
def CategoryTheory.Functor.rightOp {C : Type u₁} [] {D : Type u₂} [] (F : ) :

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
• F.rightOp = { obj := fun (X : C) => Opposite.op (F.obj ()), map := fun {X Y : C} (f : X Y) => (F.map f.op).op, map_id := , map_comp := }
Instances For
theorem CategoryTheory.Functor.rightOp_map_unop {C : Type u₁} [] {D : Type u₂} [] {F : } {X : C} {Y : C} (f : X Y) :
(F.rightOp.map f).unop = F.map f.op
instance CategoryTheory.Functor.instFullOppositeOp {C : Type u₁} [] {D : Type u₂} [] {F : } [F.Full] :
F.op.Full
Equations
• =
instance CategoryTheory.Functor.instFaithfulOppositeOp {C : Type u₁} [] {D : Type u₂} [] {F : } [F.Faithful] :
F.op.Faithful
Equations
• =
instance CategoryTheory.Functor.rightOp_faithful {C : Type u₁} [] {D : Type u₂} [] {F : } [F.Faithful] :
F.rightOp.Faithful

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

Equations
• =
instance CategoryTheory.Functor.leftOp_faithful {C : Type u₁} [] {D : Type u₂} [] {F : } [F.Faithful] :
F.leftOp.Faithful

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

Equations
• =
instance CategoryTheory.Functor.rightOp_full {C : Type u₁} [] {D : Type u₂} [] {F : } [F.Full] :
F.rightOp.Full
Equations
• =
instance CategoryTheory.Functor.leftOp_full {C : Type u₁} [] {D : Type u₂} [] {F : } [F.Full] :
F.leftOp.Full
Equations
• =
@[simp]
theorem CategoryTheory.Functor.leftOpRightOpIso_inv_app {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
F.leftOpRightOpIso.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
@[simp]
theorem CategoryTheory.Functor.leftOpRightOpIso_hom_app {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
F.leftOpRightOpIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
def CategoryTheory.Functor.leftOpRightOpIso {C : Type u₁} [] {D : Type u₂} [] (F : ) :
F.leftOp.rightOp F

The isomorphism between F.leftOp.rightOp and F.

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.rightOpLeftOpIso_hom_app {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : Cᵒᵖ) :
F.rightOpLeftOpIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
@[simp]
theorem CategoryTheory.Functor.rightOpLeftOpIso_inv_app {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : Cᵒᵖ) :
F.rightOpLeftOpIso.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
def CategoryTheory.Functor.rightOpLeftOpIso {C : Type u₁} [] {D : Type u₂} [] (F : ) :
F.rightOp.leftOp F

The isomorphism between F.rightOp.leftOp and F.

Equations
Instances For
theorem CategoryTheory.Functor.rightOp_leftOp_eq {C : Type u₁} [] {D : Type u₂} [] (F : ) :
F.rightOp.leftOp = F

Whenever possible, it is advisable to use the isomorphism rightOpLeftOpIso instead of this equality of functors.

@[simp]
theorem CategoryTheory.NatTrans.op_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F G) (X : Cᵒᵖ) :
.app X = (α.app ()).op
def CategoryTheory.NatTrans.op {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F G) :
G.op F.op

The opposite of a natural transformation.

Equations
• = { app := fun (X : Cᵒᵖ) => (α.app ()).op, naturality := }
Instances For
@[simp]
theorem CategoryTheory.NatTrans.op_id {C : Type u₁} [] {D : Type u₂} [] (F : ) :
@[simp]
theorem CategoryTheory.NatTrans.unop_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F G) (X : C) :
.app X = (α.app ()).unop
def CategoryTheory.NatTrans.unop {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F G) :
G.unop F.unop

The "unopposite" of a natural transformation.

Equations
• = { app := fun (X : C) => (α.app ()).unop, naturality := }
Instances For
@[simp]
theorem CategoryTheory.NatTrans.unop_id {C : Type u₁} [] {D : Type u₂} [] (F : ) :
@[simp]
theorem CategoryTheory.NatTrans.removeOp_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F.op G.op) (X : C) :
.app X = (α.app ()).unop
def CategoryTheory.NatTrans.removeOp {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : 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
• = { app := fun (X : C) => (α.app ()).unop, naturality := }
Instances For
@[simp]
theorem CategoryTheory.NatTrans.removeOp_id {C : Type u₁} [] {D : Type u₂} [] (F : ) :
@[simp]
theorem CategoryTheory.NatTrans.removeUnop_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F.unop G.unop) (X : Cᵒᵖ) :
X = (α.app ()).op
def CategoryTheory.NatTrans.removeUnop {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : 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
• = { app := fun (X : Cᵒᵖ) => (α.app ()).op, naturality := }
Instances For
@[simp]
theorem CategoryTheory.NatTrans.removeUnop_id {C : Type u₁} [] {D : Type u₂} [] (F : ) :
@[simp]
theorem CategoryTheory.NatTrans.leftOp_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F G) (X : Cᵒᵖ) :
.app X = (α.app ()).unop
def CategoryTheory.NatTrans.leftOp {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F G) :
G.leftOp F.leftOp

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

Equations
• = { app := fun (X : Cᵒᵖ) => (α.app ()).unop, naturality := }
Instances For
@[simp]
theorem CategoryTheory.NatTrans.leftOp_id {C : Type u₁} [] {D : Type u₂} [] {F : } :
@[simp]
theorem CategoryTheory.NatTrans.leftOp_comp {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {H : } (α : F G) (β : G H) :
@[simp]
theorem CategoryTheory.NatTrans.removeLeftOp_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F.leftOp G.leftOp) (X : C) :
X = (α.app ()).op
def CategoryTheory.NatTrans.removeLeftOp {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F.leftOp G.leftOp) :
G F

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

Equations
• = { app := fun (X : C) => (α.app ()).op, naturality := }
Instances For
@[simp]
theorem CategoryTheory.NatTrans.removeLeftOp_id {C : Type u₁} [] {D : Type u₂} [] {F : } :
@[simp]
theorem CategoryTheory.NatTrans.rightOp_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F G) (X : C) :
.app X = (α.app ()).op
def CategoryTheory.NatTrans.rightOp {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F G) :
G.rightOp F.rightOp

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

Equations
• = { app := fun (X : C) => (α.app ()).op, naturality := }
Instances For
@[simp]
theorem CategoryTheory.NatTrans.rightOp_id {C : Type u₁} [] {D : Type u₂} [] {F : } :
@[simp]
theorem CategoryTheory.NatTrans.rightOp_comp {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {H : } (α : F G) (β : G H) :
@[simp]
theorem CategoryTheory.NatTrans.removeRightOp_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F.rightOp G.rightOp) (X : Cᵒᵖ) :
= (α.app ()).unop
def CategoryTheory.NatTrans.removeRightOp {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F.rightOp G.rightOp) :
G F

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

Equations
• = { app := fun (X : Cᵒᵖ) => (α.app ()).unop, naturality := }
Instances For
@[simp]
theorem CategoryTheory.NatTrans.removeRightOp_id {C : Type u₁} [] {D : Type u₂} [] {F : } :
@[simp]
theorem CategoryTheory.Iso.op_hom {C : Type u₁} [] {X : C} {Y : C} (α : X Y) :
α.op.hom = α.hom.op
@[simp]
theorem CategoryTheory.Iso.op_inv {C : Type u₁} [] {X : C} {Y : C} (α : X Y) :
α.op.inv = α.inv.op
def CategoryTheory.Iso.op {C : Type u₁} [] {X : C} {Y : C} (α : X Y) :

The opposite isomorphism.

Equations
• α.op = { hom := α.hom.op, inv := α.inv.op, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem CategoryTheory.Iso.unop_hom {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
f.unop.hom = f.hom.unop
@[simp]
theorem CategoryTheory.Iso.unop_inv {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
f.unop.inv = f.inv.unop
def CategoryTheory.Iso.unop {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :

The isomorphism obtained from an isomorphism in the opposite category.

Equations
• f.unop = { hom := f.hom.unop, inv := f.inv.unop, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem CategoryTheory.Iso.unop_op {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
f.unop.op = f
@[simp]
theorem CategoryTheory.Iso.op_unop {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
f.op.unop = f
@[simp]
theorem CategoryTheory.Iso.unop_hom_inv_id_app_assoc {C : Type u₁} [] {D : Type u_1} [] {F : } {G : } (e : F G) (X : C) {Z : D} (h : Opposite.unop (G.obj X) Z) :
CategoryTheory.CategoryStruct.comp (e.hom.app X).unop (CategoryTheory.CategoryStruct.comp (e.inv.app X).unop h) = h
@[simp]
theorem CategoryTheory.Iso.unop_hom_inv_id_app {C : Type u₁} [] {D : Type u_1} [] {F : } {G : } (e : F G) (X : C) :
@[simp]
theorem CategoryTheory.Iso.unop_inv_hom_id_app_assoc {C : Type u₁} [] {D : Type u_1} [] {F : } {G : } (e : F G) (X : C) {Z : D} (h : Opposite.unop (F.obj X) Z) :
CategoryTheory.CategoryStruct.comp (e.inv.app X).unop (CategoryTheory.CategoryStruct.comp (e.hom.app X).unop h) = h
@[simp]
theorem CategoryTheory.Iso.unop_inv_hom_id_app {C : Type u₁} [] {D : Type u_1} [] {F : } {G : } (e : F G) (X : C) :
@[simp]
theorem CategoryTheory.NatIso.op_inv {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F G) :
.inv =
@[simp]
theorem CategoryTheory.NatIso.op_hom {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F G) :
.hom =
def CategoryTheory.NatIso.op {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : 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
• = { hom := , inv := , hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem CategoryTheory.NatIso.removeOp_inv {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F.op G.op) :
@[simp]
theorem CategoryTheory.NatIso.removeOp_hom {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F.op G.op) :
def CategoryTheory.NatIso.removeOp {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : 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
• = { hom := , inv := , hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem CategoryTheory.NatIso.unop_hom {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F G) :
.hom =
@[simp]
theorem CategoryTheory.NatIso.unop_inv {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F G) :
.inv =
def CategoryTheory.NatIso.unop {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : 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
• = { hom := , inv := , hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem CategoryTheory.Equivalence.op_unitIso {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
e.op.unitIso = (CategoryTheory.NatIso.op e.unitIso).symm
@[simp]
theorem CategoryTheory.Equivalence.op_functor {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
e.op.functor = e.functor.op
@[simp]
theorem CategoryTheory.Equivalence.op_counitIso {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
e.op.counitIso = (CategoryTheory.NatIso.op e.counitIso).symm
@[simp]
theorem CategoryTheory.Equivalence.op_inverse {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
e.op.inverse = e.inverse.op
def CategoryTheory.Equivalence.op {C : Type u₁} [] {D : Type u₂} [] (e : C D) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Equivalence.unop_counitIso {C : Type u₁} [] {D : Type u₂} [] (e : Cᵒᵖ Dᵒᵖ) :
e.unop.counitIso = (CategoryTheory.NatIso.unop e.counitIso).symm
@[simp]
theorem CategoryTheory.Equivalence.unop_inverse {C : Type u₁} [] {D : Type u₂} [] (e : Cᵒᵖ Dᵒᵖ) :
e.unop.inverse = e.inverse.unop
@[simp]
theorem CategoryTheory.Equivalence.unop_unitIso {C : Type u₁} [] {D : Type u₂} [] (e : Cᵒᵖ Dᵒᵖ) :
e.unop.unitIso = (CategoryTheory.NatIso.unop e.unitIso).symm
@[simp]
theorem CategoryTheory.Equivalence.unop_functor {C : Type u₁} [] {D : Type u₂} [] (e : Cᵒᵖ Dᵒᵖ) :
e.unop.functor = e.functor.unop
def CategoryTheory.Equivalence.unop {C : Type u₁} [] {D : Type u₂} [] (e : Cᵒᵖ Dᵒᵖ) :
C D

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.opEquiv_apply {C : Type u₁} [] (A : Cᵒᵖ) (B : Cᵒᵖ) (f : A B) :
() f = f.unop
@[simp]
theorem CategoryTheory.opEquiv_symm_apply {C : Type u₁} [] (A : Cᵒᵖ) (B : Cᵒᵖ) (g : ) :
().symm g = g.op
def CategoryTheory.opEquiv {C : Type u₁} [] (A : Cᵒᵖ) (B : Cᵒᵖ) :
(A B) ()

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 opEquiv' (A : C) (B : Cᵒᵖ) : (Opposite.op A ⟶ B) ≃ (B.unop ⟶ A) :=
opEquiv _ _

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

def opEquiv''' (A B : C) : (Opposite.op A ⟶ Opposite.op B) ≃ (B ⟶ A) :=
opEquiv _ _

Equations
• = { toFun := fun (f : A B) => f.unop, invFun := fun (g : ) => g.op, left_inv := , right_inv := }
Instances For
instance CategoryTheory.subsingleton_of_unop {C : Type u₁} [] (A : Cᵒᵖ) (B : Cᵒᵖ) [] :
Equations
• =
instance CategoryTheory.decidableEqOfUnop {C : Type u₁} [] (A : Cᵒᵖ) (B : Cᵒᵖ) [] :
Equations
• = ().decidableEq
@[simp]
theorem CategoryTheory.isoOpEquiv_apply {C : Type u₁} [] (A : Cᵒᵖ) (B : Cᵒᵖ) (f : A B) :
f = f.unop
@[simp]
theorem CategoryTheory.isoOpEquiv_symm_apply {C : Type u₁} [] (A : Cᵒᵖ) (B : Cᵒᵖ) (g : ) :
.symm g = g.op
def CategoryTheory.isoOpEquiv {C : Type u₁} [] (A : Cᵒᵖ) (B : Cᵒᵖ) :
(A B) ()

The equivalence between isomorphisms of the form A ≅ B and B.unop ≅ A.unop.

Note this is definitionally the same as the other three variants:

• (Opposite.op A ≅ B) ≃ (B.unop ≅ A)
• (A ≅ Opposite.op B) ≃ (B ≅ A.unop)
• (Opposite.op A ≅ Opposite.op B) ≃ (B ≅ A)
Equations
• = { toFun := fun (f : A B) => f.unop, invFun := fun (g : ) => g.op, left_inv := , right_inv := }
Instances For
@[simp]
theorem CategoryTheory.Functor.opUnopEquiv_functor (C : Type u₁) [] (D : Type u₂) [] :
.functor =
@[simp]
theorem CategoryTheory.Functor.opUnopEquiv_inverse (C : Type u₁) [] (D : Type u₂) [] :
.inverse =
@[simp]
theorem CategoryTheory.Functor.opUnopEquiv_unitIso (C : Type u₁) [] (D : Type u₂) [] :
.unitIso = CategoryTheory.NatIso.ofComponents (fun (F : ()ᵒᵖ) => ().opUnopIso.op)
@[simp]
theorem CategoryTheory.Functor.opUnopEquiv_counitIso (C : Type u₁) [] (D : Type u₂) [] :
.counitIso = CategoryTheory.NatIso.ofComponents (fun (F : ) => F.unopOpIso)
def CategoryTheory.Functor.opUnopEquiv (C : Type u₁) [] (D : Type u₂) [] :

The equivalence of functor categories induced by op and unop.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Functor.leftOpRightOpEquiv_counitIso_hom_app_app (C : Type u₁) [] (D : Type u₂) [] (X : ) (X : C) :
(.counitIso.hom.app X✝).app X = CategoryTheory.CategoryStruct.id (X✝.obj X)
@[simp]
theorem CategoryTheory.Functor.leftOpRightOpEquiv_unitIso_inv_app (C : Type u₁) [] (D : Type u₂) [] (X : ) :
.unitIso.inv.app X = ().rightOpLeftOpIso.inv.op
@[simp]
theorem CategoryTheory.Functor.leftOpRightOpEquiv_functor_map_app (C : Type u₁) [] (D : Type u₂) [] :
∀ {X Y : } (η : X Y) (X_1 : C), (.functor.map η).app X_1 = (η.unop.app (Opposite.op X_1)).op
@[simp]
theorem CategoryTheory.Functor.leftOpRightOpEquiv_counitIso_inv_app_app (C : Type u₁) [] (D : Type u₂) [] (X : ) (X : C) :
(.counitIso.inv.app X✝).app X = CategoryTheory.CategoryStruct.id (X✝.obj X)
@[simp]
theorem CategoryTheory.Functor.leftOpRightOpEquiv_unitIso_hom_app (C : Type u₁) [] (D : Type u₂) [] (X : ) :
.unitIso.hom.app X = ().rightOpLeftOpIso.hom.op
@[simp]
theorem CategoryTheory.Functor.leftOpRightOpEquiv_functor_obj_map (C : Type u₁) [] (D : Type u₂) [] (F : ) :
∀ {X Y : C} (f : X Y), (.functor.obj F).map f = (().map f.op).op
@[simp]
theorem CategoryTheory.Functor.leftOpRightOpEquiv_inverse_map (C : Type u₁) [] (D : Type u₂) [] :
∀ {X Y : } (η : X Y), .inverse.map η =
@[simp]
theorem CategoryTheory.Functor.leftOpRightOpEquiv_functor_obj_obj (C : Type u₁) [] (D : Type u₂) [] (F : ) (X : C) :
(.functor.obj F).obj X = Opposite.op (().obj ())
@[simp]
theorem CategoryTheory.Functor.leftOpRightOpEquiv_inverse_obj (C : Type u₁) [] (D : Type u₂) [] (F : ) :
.inverse.obj F = Opposite.op F.leftOp
def CategoryTheory.Functor.leftOpRightOpEquiv (C : Type u₁) [] (D : Type u₂) [] :

The equivalence of functor categories induced by leftOp and rightOp.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Functor.instEssSurjOppositeOp (C : Type u₁) [] (D : Type u₂) [] {F : } [F.EssSurj] :
F.op.EssSurj
Equations
• =
instance CategoryTheory.Functor.instEssSurjOppositeRightOp (C : Type u₁) [] (D : Type u₂) [] {F : } [F.EssSurj] :
F.rightOp.EssSurj
Equations
• =
instance CategoryTheory.Functor.instEssSurjOppositeLeftOp (C : Type u₁) [] (D : Type u₂) [] {F : } [F.EssSurj] :
F.leftOp.EssSurj
Equations
• =
instance CategoryTheory.Functor.instIsEquivalenceOppositeOp (C : Type u₁) [] (D : Type u₂) [] {F : } [F.IsEquivalence] :
F.op.IsEquivalence
Equations
• =
instance CategoryTheory.Functor.instIsEquivalenceOppositeRightOp (C : Type u₁) [] (D : Type u₂) [] {F : } [F.IsEquivalence] :
F.rightOp.IsEquivalence
Equations
• =
instance CategoryTheory.Functor.instIsEquivalenceOppositeLeftOp (C : Type u₁) [] (D : Type u₂) [] {F : } [F.IsEquivalence] :
F.leftOp.IsEquivalence
Equations
• =