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₁} [Quiver C] {X Y : C} : Function.Injective op

theorem Quiver.Hom.unop_inj {C : Type u₁} [Quiver C] {X Y : Cᵒᵖ} : Function.Injective unop

@[simp]

theorem Quiver.Hom.unop_op {C : Type u₁} [Quiver C] {X Y : C} (f : X ⟶ Y) : f.op.unop = f

@[simp]

theorem Quiver.Hom.unop_op' {C : Type u₁} [Quiver C] {X Y : Cᵒᵖ} {x : Opposite.unop Y ⟶ Opposite.unop X} : unop (Opposite.op x) = x

@[simp]

theorem Quiver.Hom.op_unop {C : Type u₁} [Quiver C] {X Y : Cᵒᵖ} (f : X ⟶ Y) : f.unop.op = f

@[simp]

theorem Quiver.Hom.unop_mk {C : Type u₁} [Quiver C] {X Y : Cᵒᵖ} (f : X ⟶ Y) : unop (Opposite.op f) = f

instance CategoryTheory.Category.opposite {C : Type u₁} [Category.{v₁, u₁} C] : Category.{v₁, u₁} Cᵒᵖ

The opposite category.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.op_comp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} : (CategoryStruct.comp f g).op = CategoryStruct.comp g.op f.op

theorem CategoryTheory.op_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {Z✝ : Cᵒᵖ} (h : Opposite.op X ⟶ Z✝) : CategoryStruct.comp (CategoryStruct.comp f g).op h = CategoryStruct.comp g.op (CategoryStruct.comp f.op h)

@[simp]

theorem CategoryTheory.op_id {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : (CategoryStruct.id X).op = CategoryStruct.id (Opposite.op X)

@[simp]

theorem CategoryTheory.unop_comp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} : (CategoryStruct.comp f g).unop = CategoryStruct.comp g.unop f.unop

theorem CategoryTheory.unop_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} {Z✝ : C} (h : Opposite.unop X ⟶ Z✝) : CategoryStruct.comp (CategoryStruct.comp f g).unop h = CategoryStruct.comp g.unop (CategoryStruct.comp f.unop h)

@[simp]

theorem CategoryTheory.unop_id {C : Type u₁} [Category.{v₁, u₁} C] {X : Cᵒᵖ} : (CategoryStruct.id X).unop = CategoryStruct.id (Opposite.unop X)

@[simp]

theorem CategoryTheory.unop_id_op {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : (CategoryStruct.id (Opposite.op X)).unop = CategoryStruct.id X

@[simp]

theorem CategoryTheory.op_id_unop {C : Type u₁} [Category.{v₁, u₁} C] {X : Cᵒᵖ} : (CategoryStruct.id (Opposite.unop X)).op = CategoryStruct.id X

def CategoryTheory.unopUnop (C : Type u₁) [Category.{v₁, u₁} C] : Functor Cᵒᵖᵒᵖ C

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

Equations

• CategoryTheory.unopUnop C = { obj := fun (X : Cᵒᵖᵒᵖ) => Opposite.unop (Opposite.unop X), map := fun {X Y : Cᵒᵖᵒᵖ} (f : X ⟶ Y) => f.unop.unop, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.unopUnop_obj (C : Type u₁) [Category.{v₁, u₁} C] (X : Cᵒᵖᵒᵖ) : (unopUnop C).obj X = Opposite.unop (Opposite.unop X)

@[simp]

theorem CategoryTheory.unopUnop_map (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : Cᵒᵖᵒᵖ} (f : X✝ ⟶ Y✝) : (unopUnop C).map f = f.unop.unop

def CategoryTheory.opOp (C : Type u₁) [Category.{v₁, u₁} C] : Functor C Cᵒᵖᵒᵖ

The functor from a category to its double-opposite.

Equations

• CategoryTheory.opOp C = { obj := fun (X : C) => Opposite.op (Opposite.op X), map := fun {X Y : C} (f : X ⟶ Y) => f.op.op, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.opOp_map (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (opOp C).map f = f.op.op

@[simp]

theorem CategoryTheory.opOp_obj (C : Type u₁) [Category.{v₁, u₁} C] (X : C) : (opOp C).obj X = Opposite.op (Opposite.op X)

def CategoryTheory.opOpEquivalence (C : Type u₁) [Category.{v₁, u₁} C] : Cᵒᵖᵒᵖ ≌ C

The double opposite category is equivalent to the original.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.opOpEquivalence_unitIso (C : Type u₁) [Category.{v₁, u₁} C] : (opOpEquivalence C).unitIso = Iso.refl (Functor.id Cᵒᵖᵒᵖ)

@[simp]

theorem CategoryTheory.opOpEquivalence_counitIso (C : Type u₁) [Category.{v₁, u₁} C] : (opOpEquivalence C).counitIso = Iso.refl ((opOp C).comp (unopUnop C))

@[simp]

theorem CategoryTheory.opOpEquivalence_inverse (C : Type u₁) [Category.{v₁, u₁} C] : (opOpEquivalence C).inverse = opOp C

@[simp]

theorem CategoryTheory.opOpEquivalence_functor (C : Type u₁) [Category.{v₁, u₁} C] : (opOpEquivalence C).functor = unopUnop C

instance CategoryTheory.instIsEquivalenceOppositeOpOp (C : Type u₁) [Category.{v₁, u₁} C] : (opOp C).IsEquivalence

instance CategoryTheory.instIsEquivalenceOppositeUnopUnop (C : Type u₁) [Category.{v₁, u₁} C] : (unopUnop C).IsEquivalence

instance CategoryTheory.isIso_op {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsIso f] : IsIso f.op

If f is an isomorphism, so is f.op

theorem CategoryTheory.isIso_of_op {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsIso f.op] : IsIso f

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₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : IsIso f.op ↔ IsIso f

theorem CategoryTheory.isIso_unop_iff {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y) : IsIso f.unop ↔ IsIso f

instance CategoryTheory.isIso_unop {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y) [IsIso f] : IsIso f.unop

@[simp]

theorem CategoryTheory.op_inv {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsIso f] : (inv f).op = inv f.op

@[simp]

theorem CategoryTheory.unop_inv {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y) [IsIso f] : (inv f).unop = inv f.unop

def CategoryTheory.Functor.op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Functor 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

• F.op = { obj := fun (X : Cᵒᵖ) => Opposite.op (F.obj (Opposite.unop X)), map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) => (F.map f.unop).op, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.Functor.op_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : F.op.map f = (F.map f.unop).op

@[simp]

theorem CategoryTheory.Functor.op_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : Cᵒᵖ) : F.op.obj X = Opposite.op (F.obj (Opposite.unop X))

def CategoryTheory.Functor.unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) : Functor 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

• F.unop = { obj := fun (X : C) => Opposite.unop (F.obj (Opposite.op X)), map := fun {X Y : C} (f : X ⟶ Y) => (F.map f.op).unop, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.Functor.unop_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) (X : C) : F.unop.obj X = Opposite.unop (F.obj (Opposite.op X))

@[simp]

theorem CategoryTheory.Functor.unop_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : F.unop.map f = (F.map f.op).unop

def CategoryTheory.Functor.opUnopIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : F.op.unop ≅ F

The isomorphism between F.op.unop and F.

Equations

• F.opUnopIso = CategoryTheory.NatIso.ofComponents (fun (x : C) => CategoryTheory.Iso.refl (F.op.unop.obj x)) ⋯

@[simp]

theorem CategoryTheory.Functor.opUnopIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) : F.opUnopIso.hom.app X = CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.Functor.opUnopIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) : F.opUnopIso.inv.app X = CategoryStruct.id (F.obj X)

def CategoryTheory.Functor.unopOpIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) : F.unop.op ≅ F

The isomorphism between F.unop.op and F.

Equations

• F.unopOpIso = CategoryTheory.NatIso.ofComponents (fun (x : Cᵒᵖ) => CategoryTheory.Iso.refl (F.unop.op.obj x)) ⋯

@[simp]

theorem CategoryTheory.Functor.unopOpIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) (X : Cᵒᵖ) : F.unopOpIso.hom.app X = CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.Functor.unopOpIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) (X : Cᵒᵖ) : F.unopOpIso.inv.app X = CategoryStruct.id (F.obj X)

def CategoryTheory.Functor.opHom (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : Functor (Functor C D)ᵒᵖ (Functor Cᵒᵖ Dᵒᵖ)

Taking the opposite of a functor is functorial.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.opHom_map_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ : (Functor C D)ᵒᵖ} (α : X✝ ⟶ Y✝) (X : Cᵒᵖ) : ((opHom C D).map α).app X = (α.unop.app (Opposite.unop X)).op

@[simp]

theorem CategoryTheory.Functor.opHom_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (F : (Functor C D)ᵒᵖ) : (opHom C D).obj F = (Opposite.unop F).op

def CategoryTheory.Functor.opInv (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : Functor (Functor Cᵒᵖ Dᵒᵖ) (Functor C D)ᵒᵖ

Take the "unopposite" of a functor is functorial.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.opInv_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ : Functor Cᵒᵖ Dᵒᵖ} (α : X✝ ⟶ Y✝) : (opInv C D).map α = Quiver.Hom.op { app := fun (X : C) => (α.app (Opposite.op X)).unop, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Functor.opInv_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) : (opInv C D).obj F = Opposite.op F.unop

def CategoryTheory.Functor.opComp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{u_2, u_1} E] (F : Functor C D) (G : Functor D E) : (F.comp G).op ≅ F.op.comp G.op

Compatibility of Functor.op with respect to functor composition.

Equations

• F.opComp G = CategoryTheory.Iso.refl (F.comp G).op

@[simp]

theorem CategoryTheory.Functor.opComp_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{u_2, u_1} E] (F : Functor C D) (G : Functor D E) (X : Cᵒᵖ) : (F.opComp G).hom.app X = CategoryStruct.id (Opposite.op (G.obj (F.obj (Opposite.unop X))))

@[simp]

theorem CategoryTheory.Functor.opComp_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{u_2, u_1} E] (F : Functor C D) (G : Functor D E) (X : Cᵒᵖ) : (F.opComp G).inv.app X = CategoryStruct.id (Opposite.op (G.obj (F.obj (Opposite.unop X))))

def CategoryTheory.Functor.unopComp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{u_2, u_1} E] (F : Functor Cᵒᵖ Dᵒᵖ) (G : Functor Dᵒᵖ Eᵒᵖ) : (F.comp G).unop ≅ F.unop.comp G.unop

Compatibility of Functor.unop with respect to functor composition.

Equations

• F.unopComp G = CategoryTheory.Iso.refl (F.comp G).unop

@[simp]

theorem CategoryTheory.Functor.unopComp_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{u_2, u_1} E] (F : Functor Cᵒᵖ Dᵒᵖ) (G : Functor Dᵒᵖ Eᵒᵖ) (X : C) : (F.unopComp G).inv.app X = CategoryStruct.id (Opposite.unop (G.obj (F.obj (Opposite.op X))))

@[simp]

theorem CategoryTheory.Functor.unopComp_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{u_2, u_1} E] (F : Functor Cᵒᵖ Dᵒᵖ) (G : Functor Dᵒᵖ Eᵒᵖ) (X : C) : (F.unopComp G).hom.app X = CategoryStruct.id (Opposite.unop (G.obj (F.obj (Opposite.op X))))

def CategoryTheory.Functor.opId (C : Type u₁) [Category.{v₁, u₁} C] : (Functor.id C).op ≅ Functor.id Cᵒᵖ

Functor.op transforms identity functors to identity functors.

Equations

• CategoryTheory.Functor.opId C = CategoryTheory.Iso.refl (CategoryTheory.Functor.id C).op

@[simp]

theorem CategoryTheory.Functor.opId_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (X : Cᵒᵖ) : (opId C).hom.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Functor.opId_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (X : Cᵒᵖ) : (opId C).inv.app X = CategoryStruct.id X

def CategoryTheory.Functor.unopId (C : Type u₁) [Category.{v₁, u₁} C] : (Functor.id Cᵒᵖ).unop ≅ Functor.id C

Functor.unop transforms identity functors to identity functors.

Equations

• CategoryTheory.Functor.unopId C = CategoryTheory.Iso.refl (CategoryTheory.Functor.id Cᵒᵖ).unop

@[simp]

theorem CategoryTheory.Functor.unopId_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (X : C) : (unopId C).hom.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Functor.unopId_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (X : C) : (unopId C).inv.app X = CategoryStruct.id X

def CategoryTheory.Functor.leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) : Functor 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

• F.leftOp = { obj := fun (X : Cᵒᵖ) => Opposite.unop (F.obj (Opposite.unop X)), map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) => (F.map f.unop).unop, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.Functor.leftOp_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : F.leftOp.map f = (F.map f.unop).unop

@[simp]

theorem CategoryTheory.Functor.leftOp_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) (X : Cᵒᵖ) : F.leftOp.obj X = Opposite.unop (F.obj (Opposite.unop X))

def CategoryTheory.Functor.rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) : Functor 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

• F.rightOp = { obj := fun (X : C) => Opposite.op (F.obj (Opposite.op X)), map := fun {X Y : C} (f : X ⟶ Y) => (F.map f.op).op, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.Functor.rightOp_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : F.rightOp.map f = (F.map f.op).op

@[simp]

theorem CategoryTheory.Functor.rightOp_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) (X : C) : F.rightOp.obj X = Opposite.op (F.obj (Opposite.op X))

theorem CategoryTheory.Functor.rightOp_map_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor Cᵒᵖ D} {X Y : C} (f : X ⟶ Y) : (F.rightOp.map f).unop = F.map f.op

instance CategoryTheory.Functor.instFullOppositeOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} [F.Full] : F.op.Full

instance CategoryTheory.Functor.instFaithfulOppositeOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} [F.Faithful] : F.op.Faithful

def CategoryTheory.Functor.FullyFaithful.op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) : F.op.FullyFaithful

The opposite of a fully faithful functor is fully faithful.

Equations

• hF.op = { preimage := fun {X Y : Cᵒᵖ} (f : F.op.obj X ⟶ F.op.obj Y) => (hF.preimage f.unop).op, map_preimage := ⋯, preimage_map := ⋯ }

instance CategoryTheory.Functor.rightOp_faithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor Cᵒᵖ D} [F.Faithful] : F.rightOp.Faithful

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

instance CategoryTheory.Functor.leftOp_faithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C Dᵒᵖ} [F.Faithful] : F.leftOp.Faithful

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

instance CategoryTheory.Functor.rightOp_full {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor Cᵒᵖ D} [F.Full] : F.rightOp.Full

instance CategoryTheory.Functor.leftOp_full {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C Dᵒᵖ} [F.Full] : F.leftOp.Full

def CategoryTheory.Functor.FullyFaithful.leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C Dᵒᵖ} (hF : F.FullyFaithful) : F.leftOp.FullyFaithful

The opposite of a fully faithful functor is fully faithful.

Equations

• hF.leftOp = { preimage := fun {X Y : Cᵒᵖ} (f : F.leftOp.obj X ⟶ F.leftOp.obj Y) => (hF.preimage f.op).op, map_preimage := ⋯, preimage_map := ⋯ }

def CategoryTheory.Functor.FullyFaithful.rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor Cᵒᵖ D} (hF : F.FullyFaithful) : F.rightOp.FullyFaithful

The opposite of a fully faithful functor is fully faithful.

Equations

• hF.rightOp = { preimage := fun {X Y : C} (f : F.rightOp.obj X ⟶ F.rightOp.obj Y) => (hF.preimage f.unop).unop, map_preimage := ⋯, preimage_map := ⋯ }

def CategoryTheory.Functor.rightOpComp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{u_2, u_1} E] (F : Functor Cᵒᵖ D) (G : Functor D E) : (F.comp G).rightOp ≅ F.rightOp.comp G.op

Compatibility of Functor.rightOp with respect to functor composition.

Equations

• F.rightOpComp G = CategoryTheory.Iso.refl (F.comp G).rightOp

@[simp]

theorem CategoryTheory.Functor.rightOpComp_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{u_2, u_1} E] (F : Functor Cᵒᵖ D) (G : Functor D E) (X : C) : (F.rightOpComp G).inv.app X = CategoryStruct.id (Opposite.op (G.obj (F.obj (Opposite.op X))))

@[simp]

theorem CategoryTheory.Functor.rightOpComp_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{u_2, u_1} E] (F : Functor Cᵒᵖ D) (G : Functor D E) (X : C) : (F.rightOpComp G).hom.app X = CategoryStruct.id (Opposite.op (G.obj (F.obj (Opposite.op X))))

def CategoryTheory.Functor.leftOpComp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{u_2, u_1} E] (F : Functor C D) (G : Functor D Eᵒᵖ) : (F.comp G).leftOp ≅ F.op.comp G.leftOp

Compatibility of Functor.leftOp with respect to functor composition.

Equations

• F.leftOpComp G = CategoryTheory.Iso.refl (F.comp G).leftOp

@[simp]

theorem CategoryTheory.Functor.leftOpComp_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{u_2, u_1} E] (F : Functor C D) (G : Functor D Eᵒᵖ) (X : Cᵒᵖ) : (F.leftOpComp G).hom.app X = CategoryStruct.id (Opposite.unop (G.obj (F.obj (Opposite.unop X))))

@[simp]

theorem CategoryTheory.Functor.leftOpComp_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{u_2, u_1} E] (F : Functor C D) (G : Functor D Eᵒᵖ) (X : Cᵒᵖ) : (F.leftOpComp G).inv.app X = CategoryStruct.id (Opposite.unop (G.obj (F.obj (Opposite.unop X))))

def CategoryTheory.Functor.rightOpId (C : Type u₁) [Category.{v₁, u₁} C] : (Functor.id Cᵒᵖ).rightOp ≅ opOp C

Functor.rightOp sends identity functors to the canonical isomorphism opOp.

Equations

• CategoryTheory.Functor.rightOpId C = CategoryTheory.Iso.refl (CategoryTheory.Functor.id Cᵒᵖ).rightOp

@[simp]

theorem CategoryTheory.Functor.rightOpId_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (X : C) : (rightOpId C).inv.app X = CategoryStruct.id (Opposite.op (Opposite.op X))

@[simp]

theorem CategoryTheory.Functor.rightOpId_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (X : C) : (rightOpId C).hom.app X = CategoryStruct.id (Opposite.op (Opposite.op X))

def CategoryTheory.Functor.leftOpId (C : Type u₁) [Category.{v₁, u₁} C] : (Functor.id Cᵒᵖ).leftOp ≅ unopUnop C

Functor.leftOp sends identity functors to the canonical isomorphism unopUnop.

Equations

• CategoryTheory.Functor.leftOpId C = CategoryTheory.Iso.refl (CategoryTheory.Functor.id Cᵒᵖ).leftOp

@[simp]

theorem CategoryTheory.Functor.leftOpId_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (X : Cᵒᵖᵒᵖ) : (leftOpId C).inv.app X = CategoryStruct.id (Opposite.unop (Opposite.unop X))

@[simp]

theorem CategoryTheory.Functor.leftOpId_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (X : Cᵒᵖᵒᵖ) : (leftOpId C).hom.app X = CategoryStruct.id (Opposite.unop (Opposite.unop X))

def CategoryTheory.Functor.leftOpRightOpIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) : F.leftOp.rightOp ≅ F

The isomorphism between F.leftOp.rightOp and F.

Equations

• F.leftOpRightOpIso = CategoryTheory.NatIso.ofComponents (fun (x : C) => CategoryTheory.Iso.refl (F.leftOp.rightOp.obj x)) ⋯

@[simp]

theorem CategoryTheory.Functor.leftOpRightOpIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) (X : C) : F.leftOpRightOpIso.hom.app X = CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.Functor.leftOpRightOpIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) (X : C) : F.leftOpRightOpIso.inv.app X = CategoryStruct.id (F.obj X)

def CategoryTheory.Functor.rightOpLeftOpIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) : F.rightOp.leftOp ≅ F

The isomorphism between F.rightOp.leftOp and F.

Equations

• F.rightOpLeftOpIso = CategoryTheory.NatIso.ofComponents (fun (x : Cᵒᵖ) => CategoryTheory.Iso.refl (F.rightOp.leftOp.obj x)) ⋯

@[simp]

theorem CategoryTheory.Functor.rightOpLeftOpIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) (X : Cᵒᵖ) : F.rightOpLeftOpIso.inv.app X = CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.Functor.rightOpLeftOpIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) (X : Cᵒᵖ) : F.rightOpLeftOpIso.hom.app X = CategoryStruct.id (F.obj X)

theorem CategoryTheory.Functor.rightOp_leftOp_eq {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) : F.rightOp.leftOp = F

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

def CategoryTheory.NatTrans.op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ⟶ G) : G.op ⟶ F.op

The opposite of a natural transformation.

Equations

• CategoryTheory.NatTrans.op α = { app := fun (X : Cᵒᵖ) => (α.app (Opposite.unop X)).op, naturality := ⋯ }

@[simp]

theorem CategoryTheory.NatTrans.op_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ⟶ G) (X : Cᵒᵖ) : (NatTrans.op α).app X = (α.app (Opposite.unop X)).op

@[simp]

theorem CategoryTheory.NatTrans.op_id {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : NatTrans.op (CategoryStruct.id F) = CategoryStruct.id F.op

@[simp]

theorem CategoryTheory.NatTrans.op_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor C D} (α : F ⟶ G) (β : G ⟶ H) : NatTrans.op (CategoryStruct.comp α β) = CategoryStruct.comp (NatTrans.op β) (NatTrans.op α)

theorem CategoryTheory.NatTrans.op_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor C D} (α : F ⟶ G) (β : G ⟶ H) {Z : Functor Cᵒᵖ Dᵒᵖ} (h : F.op ⟶ Z) : CategoryStruct.comp (NatTrans.op (CategoryStruct.comp α β)) h = CategoryStruct.comp (NatTrans.op β) (CategoryStruct.comp (NatTrans.op α) h)

theorem CategoryTheory.NatTrans.op_whiskerRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {E : Type u_1} [Category.{u_2, u_1} E] {H : Functor D E} (α : F ⟶ G) : NatTrans.op (Functor.whiskerRight α H) = CategoryStruct.comp (G.opComp H).hom (CategoryStruct.comp (Functor.whiskerRight (NatTrans.op α) H.op) (F.opComp H).inv)

theorem CategoryTheory.NatTrans.op_whiskerRight_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {E : Type u_1} [Category.{u_2, u_1} E] {H : Functor D E} (α : F ⟶ G) {Z : Functor Cᵒᵖ Eᵒᵖ} (h : (F.comp H).op ⟶ Z) : CategoryStruct.comp (NatTrans.op (Functor.whiskerRight α H)) h = CategoryStruct.comp (G.opComp H).hom (CategoryStruct.comp (Functor.whiskerRight (NatTrans.op α) H.op) (CategoryStruct.comp (F.opComp H).inv h))

theorem CategoryTheory.NatTrans.op_whiskerLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {E : Type u_1} [Category.{u_2, u_1} E] {H : Functor E C} (α : F ⟶ G) : NatTrans.op (H.whiskerLeft α) = CategoryStruct.comp (H.opComp G).hom (CategoryStruct.comp (H.op.whiskerLeft (NatTrans.op α)) (H.opComp F).inv)

theorem CategoryTheory.NatTrans.op_whiskerLeft_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {E : Type u_1} [Category.{u_2, u_1} E] {H : Functor E C} (α : F ⟶ G) {Z : Functor Eᵒᵖ Dᵒᵖ} (h : (H.comp F).op ⟶ Z) : CategoryStruct.comp (NatTrans.op (H.whiskerLeft α)) h = CategoryStruct.comp (H.opComp G).hom (CategoryStruct.comp (H.op.whiskerLeft (NatTrans.op α)) (CategoryStruct.comp (H.opComp F).inv h))

def CategoryTheory.NatTrans.unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor Cᵒᵖ Dᵒᵖ} (α : F ⟶ G) : G.unop ⟶ F.unop

The "unopposite" of a natural transformation.

Equations

• CategoryTheory.NatTrans.unop α = { app := fun (X : C) => (α.app (Opposite.op X)).unop, naturality := ⋯ }

@[simp]

theorem CategoryTheory.NatTrans.unop_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor Cᵒᵖ Dᵒᵖ} (α : F ⟶ G) (X : C) : (NatTrans.unop α).app X = (α.app (Opposite.op X)).unop

@[simp]

theorem CategoryTheory.NatTrans.unop_id {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) : NatTrans.unop (CategoryStruct.id F) = CategoryStruct.id F.unop

@[simp]

theorem CategoryTheory.NatTrans.unop_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor Cᵒᵖ Dᵒᵖ} (α : F ⟶ G) (β : G ⟶ H) : NatTrans.unop (CategoryStruct.comp α β) = CategoryStruct.comp (NatTrans.unop β) (NatTrans.unop α)

theorem CategoryTheory.NatTrans.unop_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor Cᵒᵖ Dᵒᵖ} (α : F ⟶ G) (β : G ⟶ H) {Z : Functor C D} (h : F.unop ⟶ Z) : CategoryStruct.comp (NatTrans.unop (CategoryStruct.comp α β)) h = CategoryStruct.comp (NatTrans.unop β) (CategoryStruct.comp (NatTrans.unop α) h)

theorem CategoryTheory.NatTrans.unop_whiskerRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor Cᵒᵖ Dᵒᵖ} {E : Type u_1} [Category.{u_2, u_1} E] {H : Functor Dᵒᵖ Eᵒᵖ} (α : F ⟶ G) : NatTrans.unop (Functor.whiskerRight α H) = CategoryStruct.comp (G.unopComp H).hom (CategoryStruct.comp (Functor.whiskerRight (NatTrans.unop α) H.unop) (F.unopComp H).inv)

theorem CategoryTheory.NatTrans.unop_whiskerRight_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor Cᵒᵖ Dᵒᵖ} {E : Type u_1} [Category.{u_2, u_1} E] {H : Functor Dᵒᵖ Eᵒᵖ} (α : F ⟶ G) {Z : Functor C E} (h : (F.comp H).unop ⟶ Z) : CategoryStruct.comp (NatTrans.unop (Functor.whiskerRight α H)) h = CategoryStruct.comp (G.unopComp H).hom (CategoryStruct.comp (Functor.whiskerRight (NatTrans.unop α) H.unop) (CategoryStruct.comp (F.unopComp H).inv h))

theorem CategoryTheory.NatTrans.unop_whiskerLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor Cᵒᵖ Dᵒᵖ} {E : Type u_1} [Category.{u_2, u_1} E] {H : Functor Eᵒᵖ Cᵒᵖ} (α : F ⟶ G) : NatTrans.unop (H.whiskerLeft α) = CategoryStruct.comp (H.unopComp G).hom (CategoryStruct.comp (H.unop.whiskerLeft (NatTrans.unop α)) (H.unopComp F).inv)

theorem CategoryTheory.NatTrans.unop_whiskerLeft_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor Cᵒᵖ Dᵒᵖ} {E : Type u_1} [Category.{u_2, u_1} E] {H : Functor Eᵒᵖ Cᵒᵖ} (α : F ⟶ G) {Z : Functor E D} (h : (H.comp F).unop ⟶ Z) : CategoryStruct.comp (NatTrans.unop (H.whiskerLeft α)) h = CategoryStruct.comp (H.unopComp G).hom (CategoryStruct.comp (H.unop.whiskerLeft (NatTrans.unop α)) (CategoryStruct.comp (H.unopComp F).inv h))

def CategoryTheory.NatTrans.removeOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor 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

• CategoryTheory.NatTrans.removeOp α = { app := fun (X : C) => (α.app (Opposite.op X)).unop, naturality := ⋯ }

@[simp]

theorem CategoryTheory.NatTrans.removeOp_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F.op ⟶ G.op) (X : C) : (NatTrans.removeOp α).app X = (α.app (Opposite.op X)).unop

@[simp]

theorem CategoryTheory.NatTrans.removeOp_id {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : NatTrans.removeOp (CategoryStruct.id F.op) = CategoryStruct.id F

def CategoryTheory.NatTrans.removeUnop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor 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

• CategoryTheory.NatTrans.removeUnop α = { app := fun (X : Cᵒᵖ) => (α.app (Opposite.unop X)).op, naturality := ⋯ }

@[simp]

theorem CategoryTheory.NatTrans.removeUnop_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor Cᵒᵖ Dᵒᵖ} (α : F.unop ⟶ G.unop) (X : Cᵒᵖ) : (NatTrans.removeUnop α).app X = (α.app (Opposite.unop X)).op

@[simp]

theorem CategoryTheory.NatTrans.removeUnop_id {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) : NatTrans.removeUnop (CategoryStruct.id F.unop) = CategoryStruct.id F

def CategoryTheory.NatTrans.leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C Dᵒᵖ} (α : 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

• CategoryTheory.NatTrans.leftOp α = { app := fun (X : Cᵒᵖ) => (α.app (Opposite.unop X)).unop, naturality := ⋯ }

@[simp]

theorem CategoryTheory.NatTrans.leftOp_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C Dᵒᵖ} (α : F ⟶ G) (X : Cᵒᵖ) : (NatTrans.leftOp α).app X = (α.app (Opposite.unop X)).unop

@[simp]

theorem CategoryTheory.NatTrans.leftOp_id {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C Dᵒᵖ} : NatTrans.leftOp (CategoryStruct.id F) = CategoryStruct.id F.leftOp

@[simp]

theorem CategoryTheory.NatTrans.leftOp_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor C Dᵒᵖ} (α : F ⟶ G) (β : G ⟶ H) : NatTrans.leftOp (CategoryStruct.comp α β) = CategoryStruct.comp (NatTrans.leftOp β) (NatTrans.leftOp α)

theorem CategoryTheory.NatTrans.leftOpWhiskerRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C Dᵒᵖ} {E : Type u_1} [Category.{u_2, u_1} E] {H : Functor E C} (α : F ⟶ G) : NatTrans.leftOp (H.whiskerLeft α) = CategoryStruct.comp (H.leftOpComp G).hom (CategoryStruct.comp (H.op.whiskerLeft (NatTrans.leftOp α)) (H.leftOpComp F).inv)

theorem CategoryTheory.NatTrans.leftOpWhiskerRight_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C Dᵒᵖ} {E : Type u_1} [Category.{u_2, u_1} E] {H : Functor E C} (α : F ⟶ G) {Z : Functor Eᵒᵖ D} (h : (H.comp F).leftOp ⟶ Z) : CategoryStruct.comp (NatTrans.leftOp (H.whiskerLeft α)) h = CategoryStruct.comp (H.leftOpComp G).hom (CategoryStruct.comp (H.op.whiskerLeft (NatTrans.leftOp α)) (CategoryStruct.comp (H.leftOpComp F).inv h))

def CategoryTheory.NatTrans.removeLeftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C Dᵒᵖ} (α : 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

• CategoryTheory.NatTrans.removeLeftOp α = { app := fun (X : C) => (α.app (Opposite.op X)).op, naturality := ⋯ }

@[simp]

theorem CategoryTheory.NatTrans.removeLeftOp_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C Dᵒᵖ} (α : F.leftOp ⟶ G.leftOp) (X : C) : (NatTrans.removeLeftOp α).app X = (α.app (Opposite.op X)).op

@[simp]

theorem CategoryTheory.NatTrans.removeLeftOp_id {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C Dᵒᵖ} : NatTrans.removeLeftOp (CategoryStruct.id F.leftOp) = CategoryStruct.id F

def CategoryTheory.NatTrans.rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor Cᵒᵖ D} (α : 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

• CategoryTheory.NatTrans.rightOp α = { app := fun (x : C) => (α.app (Opposite.op x)).op, naturality := ⋯ }

@[simp]

theorem CategoryTheory.NatTrans.rightOp_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor Cᵒᵖ D} (α : F ⟶ G) (x✝ : C) : (NatTrans.rightOp α).app x✝ = (α.app (Opposite.op x✝)).op

@[simp]

theorem CategoryTheory.NatTrans.rightOp_id {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor Cᵒᵖ D} : NatTrans.rightOp (CategoryStruct.id F) = CategoryStruct.id F.rightOp

@[simp]

theorem CategoryTheory.NatTrans.rightOp_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor Cᵒᵖ D} (α : F ⟶ G) (β : G ⟶ H) : NatTrans.rightOp (CategoryStruct.comp α β) = CategoryStruct.comp (NatTrans.rightOp β) (NatTrans.rightOp α)

theorem CategoryTheory.NatTrans.rightOpWhiskerRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor Cᵒᵖ D} {E : Type u_1} [Category.{u_2, u_1} E] {H : Functor D E} (α : F ⟶ G) : NatTrans.rightOp (Functor.whiskerRight α H) = CategoryStruct.comp (G.rightOpComp H).hom (CategoryStruct.comp (Functor.whiskerRight (NatTrans.rightOp α) H.op) (F.rightOpComp H).inv)

theorem CategoryTheory.NatTrans.rightOpWhiskerRight_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor Cᵒᵖ D} {E : Type u_1} [Category.{u_2, u_1} E] {H : Functor D E} (α : F ⟶ G) {Z : Functor C Eᵒᵖ} (h : (F.comp H).rightOp ⟶ Z) : CategoryStruct.comp (NatTrans.rightOp (Functor.whiskerRight α H)) h = CategoryStruct.comp (G.rightOpComp H).hom (CategoryStruct.comp (Functor.whiskerRight (NatTrans.rightOp α) H.op) (CategoryStruct.comp (F.rightOpComp H).inv h))

def CategoryTheory.NatTrans.removeRightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor Cᵒᵖ D} (α : 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

• CategoryTheory.NatTrans.removeRightOp α = { app := fun (X : Cᵒᵖ) => (α.app (Opposite.unop X)).unop, naturality := ⋯ }

@[simp]

theorem CategoryTheory.NatTrans.removeRightOp_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor Cᵒᵖ D} (α : F.rightOp ⟶ G.rightOp) (X : Cᵒᵖ) : (NatTrans.removeRightOp α).app X = (α.app (Opposite.unop X)).unop

@[simp]

theorem CategoryTheory.NatTrans.removeRightOp_id {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor Cᵒᵖ D} : NatTrans.removeRightOp (CategoryStruct.id F.rightOp) = CategoryStruct.id F

def CategoryTheory.Iso.op {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (α : X ≅ Y) : Opposite.op Y ≅ Opposite.op X

The opposite isomorphism.

Equations

• α.op = { hom := α.hom.op, inv := α.inv.op, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Iso.op_inv {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (α : X ≅ Y) : α.op.inv = α.inv.op

@[simp]

theorem CategoryTheory.Iso.op_hom {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (α : X ≅ Y) : α.op.hom = α.hom.op

def CategoryTheory.Iso.unop {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ≅ Y) : Opposite.unop Y ≅ Opposite.unop X

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 := ⋯ }

@[simp]

theorem CategoryTheory.Iso.unop_hom {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ≅ Y) : f.unop.hom = f.hom.unop

@[simp]

theorem CategoryTheory.Iso.unop_inv {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ≅ Y) : f.unop.inv = f.inv.unop

@[simp]

theorem CategoryTheory.Iso.unop_op {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ≅ Y) : f.unop.op = f

@[simp]

theorem CategoryTheory.Iso.op_unop {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ≅ Y) : f.op.unop = f

@[simp]

theorem CategoryTheory.Iso.op_refl {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : (refl X).op = refl (Opposite.op X)

@[simp]

theorem CategoryTheory.Iso.op_trans {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).op = β.op ≪≫ α.op

@[simp]

theorem CategoryTheory.Iso.op_symm {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (α : X ≅ Y) : α.symm.op = α.op.symm

@[simp]

theorem CategoryTheory.Iso.unop_refl {C : Type u₁} [Category.{v₁, u₁} C] (X : Cᵒᵖ) : (refl X).unop = refl (Opposite.unop X)

@[simp]

theorem CategoryTheory.Iso.unop_trans {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).unop = β.unop ≪≫ α.unop

@[simp]

theorem CategoryTheory.Iso.unop_symm {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (α : X ≅ Y) : α.symm.unop = α.unop.symm

@[simp]

theorem CategoryTheory.Iso.unop_hom_inv_id_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u_1} [Category.{u_2, u_1} D] {F G : Functor C Dᵒᵖ} (e : F ≅ G) (X : C) : CategoryStruct.comp (e.hom.app X).unop (e.inv.app X).unop = CategoryStruct.id (Opposite.unop (G.obj X))

@[simp]

theorem CategoryTheory.Iso.unop_hom_inv_id_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u_1} [Category.{u_2, u_1} D] {F G : Functor C Dᵒᵖ} (e : F ≅ G) (X : C) {Z : D} (h : Opposite.unop (G.obj X) ⟶ Z) : CategoryStruct.comp (e.hom.app X).unop (CategoryStruct.comp (e.inv.app X).unop h) = h

@[simp]

theorem CategoryTheory.Iso.unop_inv_hom_id_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u_1} [Category.{u_2, u_1} D] {F G : Functor C Dᵒᵖ} (e : F ≅ G) (X : C) : CategoryStruct.comp (e.inv.app X).unop (e.hom.app X).unop = CategoryStruct.id (Opposite.unop (F.obj X))

@[simp]

theorem CategoryTheory.Iso.unop_inv_hom_id_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u_1} [Category.{u_2, u_1} D] {F G : Functor C Dᵒᵖ} (e : F ≅ G) (X : C) {Z : D} (h : Opposite.unop (F.obj X) ⟶ Z) : CategoryStruct.comp (e.inv.app X).unop (CategoryStruct.comp (e.hom.app X).unop h) = h

def CategoryTheory.NatIso.op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor 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

• CategoryTheory.NatIso.op α = { hom := CategoryTheory.NatTrans.op α.hom, inv := CategoryTheory.NatTrans.op α.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.NatIso.op_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ≅ G) : (NatIso.op α).hom = NatTrans.op α.hom

@[simp]

theorem CategoryTheory.NatIso.op_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ≅ G) : (NatIso.op α).inv = NatTrans.op α.inv

@[simp]

theorem CategoryTheory.NatIso.op_refl {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} : NatIso.op (Iso.refl F) = Iso.refl F.op

@[simp]

theorem CategoryTheory.NatIso.op_trans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor C D} (α : F ≅ G) (β : G ≅ H) : NatIso.op (α ≪≫ β) = NatIso.op β ≪≫ NatIso.op α

@[simp]

theorem CategoryTheory.NatIso.op_symm {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ≅ G) : NatIso.op α.symm = (NatIso.op α).symm

def CategoryTheory.NatIso.removeOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor 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

• CategoryTheory.NatIso.removeOp α = { hom := CategoryTheory.NatTrans.removeOp α.hom, inv := CategoryTheory.NatTrans.removeOp α.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.NatIso.removeOp_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F.op ≅ G.op) : (NatIso.removeOp α).hom = NatTrans.removeOp α.hom

@[simp]

theorem CategoryTheory.NatIso.removeOp_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F.op ≅ G.op) : (NatIso.removeOp α).inv = NatTrans.removeOp α.inv

def CategoryTheory.NatIso.unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor 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

• CategoryTheory.NatIso.unop α = { hom := CategoryTheory.NatTrans.unop α.hom, inv := CategoryTheory.NatTrans.unop α.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.NatIso.unop_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor Cᵒᵖ Dᵒᵖ} (α : F ≅ G) : (NatIso.unop α).hom = NatTrans.unop α.hom

@[simp]

theorem CategoryTheory.NatIso.unop_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor Cᵒᵖ Dᵒᵖ} (α : F ≅ G) : (NatIso.unop α).inv = NatTrans.unop α.inv

@[simp]

theorem CategoryTheory.NatIso.unop_refl {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) : NatIso.unop (Iso.refl F) = Iso.refl F.unop

@[simp]

theorem CategoryTheory.NatIso.unop_trans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor Cᵒᵖ Dᵒᵖ} (α : F ≅ G) (β : G ≅ H) : NatIso.unop (α ≪≫ β) = NatIso.unop β ≪≫ NatIso.unop α

@[simp]

theorem CategoryTheory.NatIso.unop_symm {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor Cᵒᵖ Dᵒᵖ} (α : F ≅ G) : NatIso.unop α.symm = (NatIso.unop α).symm

theorem CategoryTheory.NatIso.op_isoWhiskerRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {E : Type u_1} [Category.{u_2, u_1} E] {H : Functor D E} (α : F ≅ G) : NatIso.op (Functor.isoWhiskerRight α H) = G.opComp H ≪≫ Functor.isoWhiskerRight (NatIso.op α) H.op ≪≫ (F.opComp H).symm

theorem CategoryTheory.NatIso.op_isoWhiskerLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {E : Type u_1} [Category.{u_2, u_1} E] {H : Functor E C} (α : F ≅ G) : NatIso.op (H.isoWhiskerLeft α) = H.opComp G ≪≫ H.op.isoWhiskerLeft (NatIso.op α) ≪≫ (H.opComp F).symm

theorem CategoryTheory.NatIso.unop_whiskerRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor Cᵒᵖ Dᵒᵖ} {E : Type u_1} [Category.{u_2, u_1} E] {H : Functor Dᵒᵖ Eᵒᵖ} (α : F ≅ G) : NatIso.unop (Functor.isoWhiskerRight α H) = G.unopComp H ≪≫ Functor.isoWhiskerRight (NatIso.unop α) H.unop ≪≫ (F.unopComp H).symm

theorem CategoryTheory.NatIso.unop_whiskerLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor Cᵒᵖ Dᵒᵖ} {E : Type u_1} [Category.{u_2, u_1} E] {H : Functor Eᵒᵖ Cᵒᵖ} (α : F ≅ G) : NatIso.unop (H.isoWhiskerLeft α) = H.unopComp G ≪≫ H.unop.isoWhiskerLeft (NatIso.unop α) ≪≫ (H.unopComp F).symm

theorem CategoryTheory.NatIso.op_leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} : NatIso.op F.leftUnitor = F.op.leftUnitor.symm ≪≫ Functor.isoWhiskerRight (Functor.opId C).symm F.op ≪≫ ((Functor.id C).opComp F).symm

theorem CategoryTheory.NatIso.op_rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} : NatIso.op F.rightUnitor = F.op.rightUnitor.symm ≪≫ F.op.isoWhiskerLeft (Functor.opId D).symm ≪≫ (F.opComp (Functor.id D)).symm

theorem CategoryTheory.NatIso.op_associator {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} {E' : Type u_2} [Category.{u_3, u_1} E] [Category.{u_4, u_2} E'] {F : Functor C D} {G : Functor D E} {H : Functor E E'} : NatIso.op (F.associator G H) = F.opComp (G.comp H) ≪≫ F.op.isoWhiskerLeft (G.opComp H) ≪≫ (F.op.associator G.op H.op).symm ≪≫ Functor.isoWhiskerRight (F.opComp G).symm H.op ≪≫ ((F.comp G).opComp H).symm

theorem CategoryTheory.NatIso.unop_leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor Cᵒᵖ Dᵒᵖ} : NatIso.unop F.leftUnitor = F.unop.leftUnitor.symm ≪≫ Functor.isoWhiskerRight (Functor.unopId C).symm F.unop ≪≫ ((Functor.id Cᵒᵖ).unopComp F).symm

theorem CategoryTheory.NatIso.unop_rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor Cᵒᵖ Dᵒᵖ} : NatIso.unop F.rightUnitor = F.unop.rightUnitor.symm ≪≫ F.unop.isoWhiskerLeft (Functor.unopId D).symm ≪≫ (F.unopComp (Functor.id Dᵒᵖ)).symm

theorem CategoryTheory.NatIso.unop_associator {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} {E' : Type u_2} [Category.{u_3, u_1} E] [Category.{u_4, u_2} E'] {F : Functor Cᵒᵖ Dᵒᵖ} {G : Functor Dᵒᵖ Eᵒᵖ} {H : Functor Eᵒᵖ E'ᵒᵖ} : NatIso.unop (F.associator G H) = F.unopComp (G.comp H) ≪≫ F.unop.isoWhiskerLeft (G.unopComp H) ≪≫ (F.unop.associator G.unop H.unop).symm ≪≫ Functor.isoWhiskerRight (F.unopComp G).symm H.unop ≪≫ ((F.comp G).unopComp H).symm

def CategoryTheory.Equivalence.op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : 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.

@[simp]

theorem CategoryTheory.Equivalence.op_unitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : e.op.unitIso = (NatIso.op e.unitIso).symm

@[simp]

theorem CategoryTheory.Equivalence.op_counitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : e.op.counitIso = (NatIso.op e.counitIso).symm

@[simp]

theorem CategoryTheory.Equivalence.op_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : e.op.functor = e.functor.op

@[simp]

theorem CategoryTheory.Equivalence.op_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : e.op.inverse = e.inverse.op

def CategoryTheory.Equivalence.unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (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.

@[simp]

theorem CategoryTheory.Equivalence.unop_counitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ Dᵒᵖ) : e.unop.counitIso = (NatIso.unop e.counitIso).symm

@[simp]

theorem CategoryTheory.Equivalence.unop_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ Dᵒᵖ) : e.unop.inverse = e.inverse.unop

@[simp]

theorem CategoryTheory.Equivalence.unop_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ Dᵒᵖ) : e.unop.functor = e.functor.unop

@[simp]

theorem CategoryTheory.Equivalence.unop_unitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ Dᵒᵖ) : e.unop.unitIso = (NatIso.unop e.unitIso).symm

def CategoryTheory.Equivalence.leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) : Cᵒᵖ ≌ D

An equivalence between C and Dᵒᵖ gives an equivalence between Cᵒᵖ and D.

Equations

• e.leftOp = e.op.trans (CategoryTheory.opOpEquivalence D)

@[simp]

theorem CategoryTheory.Equivalence.leftOp_inverse_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) (X : D) : e.leftOp.inverse.obj X = Opposite.op (e.inverse.obj (Opposite.op X))

@[simp]

theorem CategoryTheory.Equivalence.leftOp_inverse_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : e.leftOp.inverse.map f = (e.inverse.map f.op).op

@[simp]

theorem CategoryTheory.Equivalence.leftOp_unitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) (X : Cᵒᵖ) : e.leftOp.unitIso.inv.app X = (e.unitIso.hom.app (Opposite.unop X)).op

@[simp]

theorem CategoryTheory.Equivalence.leftOp_functor_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : e.leftOp.functor.map f = (e.functor.map f.unop).unop

@[simp]

theorem CategoryTheory.Equivalence.leftOp_unitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) (X : Cᵒᵖ) : e.leftOp.unitIso.hom.app X = (e.unitIso.inv.app (Opposite.unop X)).op

@[simp]

theorem CategoryTheory.Equivalence.leftOp_functor_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) (X : Cᵒᵖ) : e.leftOp.functor.obj X = Opposite.unop (e.functor.obj (Opposite.unop X))

@[simp]

theorem CategoryTheory.Equivalence.leftOp_counitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) (X : D) : e.leftOp.counitIso.inv.app X = (e.counitIso.hom.app (Opposite.op X)).unop

@[simp]

theorem CategoryTheory.Equivalence.leftOp_counitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) (X : D) : e.leftOp.counitIso.hom.app X = (e.counitIso.inv.app (Opposite.op X)).unop

def CategoryTheory.Equivalence.rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) : C ≌ Dᵒᵖ

An equivalence between Cᵒᵖ and D gives an equivalence between C and Dᵒᵖ.

Equations

• e.rightOp = (CategoryTheory.opOpEquivalence C).symm.trans e.op

@[simp]

theorem CategoryTheory.Equivalence.rightOp_inverse_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) {X✝ Y✝ : Dᵒᵖ} (f : X✝ ⟶ Y✝) : e.rightOp.inverse.map f = (e.inverse.map f.unop).unop

@[simp]

theorem CategoryTheory.Equivalence.rightOp_functor_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : e.rightOp.functor.map f = (e.functor.map f.op).op

@[simp]

theorem CategoryTheory.Equivalence.rightOp_functor_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) (X : C) : e.rightOp.functor.obj X = Opposite.op (e.functor.obj (Opposite.op X))

@[simp]

theorem CategoryTheory.Equivalence.rightOp_inverse_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) (X : Dᵒᵖ) : e.rightOp.inverse.obj X = Opposite.unop (e.inverse.obj (Opposite.unop X))

@[simp]

theorem CategoryTheory.Equivalence.rightOp_counitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) (X : Dᵒᵖ) : e.rightOp.counitIso.hom.app X = (e.counitIso.inv.app (Opposite.unop X)).op

@[simp]

theorem CategoryTheory.Equivalence.rightOp_counitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) (X : Dᵒᵖ) : e.rightOp.counitIso.inv.app X = (e.counitIso.hom.app (Opposite.unop X)).op

@[simp]

theorem CategoryTheory.Equivalence.rightOp_unitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) (X : C) : e.rightOp.unitIso.hom.app X = (e.unitIso.inv.app (Opposite.op X)).unop

@[simp]

theorem CategoryTheory.Equivalence.rightOp_unitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) (X : C) : e.rightOp.unitIso.inv.app X = (e.unitIso.hom.app (Opposite.op X)).unop

def CategoryTheory.opEquiv {C : Type u₁} [Category.{v₁, u₁} 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 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

• CategoryTheory.opEquiv A B = { toFun := fun (f : A ⟶ B) => f.unop, invFun := fun (g : Opposite.unop B ⟶ Opposite.unop A) => g.op, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CategoryTheory.opEquiv_apply {C : Type u₁} [Category.{v₁, u₁} C] (A B : Cᵒᵖ) (f : A ⟶ B) : (opEquiv A B) f = f.unop

@[simp]

theorem CategoryTheory.opEquiv_symm_apply {C : Type u₁} [Category.{v₁, u₁} C] (A B : Cᵒᵖ) (g : Opposite.unop B ⟶ Opposite.unop A) : (opEquiv A B).symm g = g.op

instance CategoryTheory.subsingleton_of_unop {C : Type u₁} [Category.{v₁, u₁} C] (A B : Cᵒᵖ) [Subsingleton (Opposite.unop B ⟶ Opposite.unop A)] : Subsingleton (A ⟶ B)

instance CategoryTheory.decidableEqOfUnop {C : Type u₁} [Category.{v₁, u₁} C] (A B : Cᵒᵖ) [DecidableEq (Opposite.unop B ⟶ Opposite.unop A)] : DecidableEq (A ⟶ B)

Equations

• CategoryTheory.decidableEqOfUnop A B = (CategoryTheory.opEquiv A B).decidableEq

def CategoryTheory.isoOpEquiv {C : Type u₁} [Category.{v₁, u₁} C] (A B : Cᵒᵖ) : (A ≅ B) ≃ (Opposite.unop B ≅ Opposite.unop A)

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

• CategoryTheory.isoOpEquiv A B = { toFun := fun (f : A ≅ B) => f.unop, invFun := fun (g : Opposite.unop B ≅ Opposite.unop A) => g.op, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CategoryTheory.isoOpEquiv_symm_apply {C : Type u₁} [Category.{v₁, u₁} C] (A B : Cᵒᵖ) (g : Opposite.unop B ≅ Opposite.unop A) : (isoOpEquiv A B).symm g = g.op

@[simp]

theorem CategoryTheory.isoOpEquiv_apply {C : Type u₁} [Category.{v₁, u₁} C] (A B : Cᵒᵖ) (f : A ≅ B) : (isoOpEquiv A B) f = f.unop

def CategoryTheory.Functor.opUnopEquiv (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (Functor C D)ᵒᵖ ≌ Functor Cᵒᵖ Dᵒᵖ

The equivalence of functor categories induced by op and unop.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.opUnopEquiv_functor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (opUnopEquiv C D).functor = opHom C D

@[simp]

theorem CategoryTheory.Functor.opUnopEquiv_inverse (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (opUnopEquiv C D).inverse = opInv C D

@[simp]

theorem CategoryTheory.Functor.opUnopEquiv_unitIso (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (opUnopEquiv C D).unitIso = NatIso.ofComponents (fun (F : (Functor C D)ᵒᵖ) => (Opposite.unop F).opUnopIso.op) ⋯

@[simp]

theorem CategoryTheory.Functor.opUnopEquiv_counitIso (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (opUnopEquiv C D).counitIso = NatIso.ofComponents (fun (F : Functor Cᵒᵖ Dᵒᵖ) => F.unopOpIso) ⋯

def CategoryTheory.Functor.leftOpRightOpEquiv (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (Functor Cᵒᵖ D)ᵒᵖ ≌ Functor C Dᵒᵖ

The equivalence of functor categories induced by leftOp and rightOp.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.leftOpRightOpEquiv_inverse_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ : Functor C Dᵒᵖ} (η : X✝ ⟶ Y✝) : (leftOpRightOpEquiv C D).inverse.map η = (NatTrans.leftOp η).op

@[simp]

theorem CategoryTheory.Functor.leftOpRightOpEquiv_counitIso_inv_app_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : Functor C Dᵒᵖ) (X✝ : C) : ((leftOpRightOpEquiv C D).counitIso.inv.app X).app X✝ = CategoryStruct.id (X.obj X✝)

@[simp]

theorem CategoryTheory.Functor.leftOpRightOpEquiv_unitIso_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : (Functor Cᵒᵖ D)ᵒᵖ) : (leftOpRightOpEquiv C D).unitIso.inv.app X = (Opposite.unop X).rightOpLeftOpIso.inv.op

@[simp]

theorem CategoryTheory.Functor.leftOpRightOpEquiv_functor_obj_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (F : (Functor Cᵒᵖ D)ᵒᵖ) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((leftOpRightOpEquiv C D).functor.obj F).map f = ((Opposite.unop F).map f.op).op

@[simp]

theorem CategoryTheory.Functor.leftOpRightOpEquiv_inverse_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) : (leftOpRightOpEquiv C D).inverse.obj F = Opposite.op F.leftOp

@[simp]

theorem CategoryTheory.Functor.leftOpRightOpEquiv_unitIso_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : (Functor Cᵒᵖ D)ᵒᵖ) : (leftOpRightOpEquiv C D).unitIso.hom.app X = (Opposite.unop X).rightOpLeftOpIso.hom.op

@[simp]

theorem CategoryTheory.Functor.leftOpRightOpEquiv_counitIso_hom_app_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : Functor C Dᵒᵖ) (X✝ : C) : ((leftOpRightOpEquiv C D).counitIso.hom.app X).app X✝ = CategoryStruct.id (X.obj X✝)

@[simp]

theorem CategoryTheory.Functor.leftOpRightOpEquiv_functor_obj_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (F : (Functor Cᵒᵖ D)ᵒᵖ) (X : C) : ((leftOpRightOpEquiv C D).functor.obj F).obj X = Opposite.op ((Opposite.unop F).obj (Opposite.op X))

@[simp]

theorem CategoryTheory.Functor.leftOpRightOpEquiv_functor_map_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ : (Functor Cᵒᵖ D)ᵒᵖ} (η : X✝ ⟶ Y✝) (x✝ : C) : ((leftOpRightOpEquiv C D).functor.map η).app x✝ = (η.unop.app (Opposite.op x✝)).op

instance CategoryTheory.Functor.instEssSurjOppositeOp (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {F : Functor C D} [F.EssSurj] : F.op.EssSurj

instance CategoryTheory.Functor.instEssSurjOppositeRightOp (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {F : Functor Cᵒᵖ D} [F.EssSurj] : F.rightOp.EssSurj

instance CategoryTheory.Functor.instEssSurjOppositeLeftOp (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {F : Functor C Dᵒᵖ} [F.EssSurj] : F.leftOp.EssSurj

instance CategoryTheory.Functor.instIsEquivalenceOppositeOp (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {F : Functor C D} [F.IsEquivalence] : F.op.IsEquivalence

instance CategoryTheory.Functor.instIsEquivalenceOppositeRightOp (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {F : Functor Cᵒᵖ D} [F.IsEquivalence] : F.rightOp.IsEquivalence

instance CategoryTheory.Functor.instIsEquivalenceOppositeLeftOp (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {F : Functor C Dᵒᵖ} [F.IsEquivalence] : F.leftOp.IsEquivalence