Documentation

Mathlib.CategoryTheory.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.

theorem Quiver.Hom.op_inj {C : Type u₁} [Quiver C] {X Y : C} :
@[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} :
@[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) :
@[simp]
theorem CategoryTheory.op_comp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X Y} {g : Y Z} :
@[simp]
theorem CategoryTheory.unop_comp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X Y} {g : Y Z} :

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

Equations
@[simp]
theorem CategoryTheory.unopUnop_map (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : Cᵒᵖᵒᵖ} (f : X✝ Y✝) :

The functor from a category to its double-opposite.

Equations
@[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]

The double opposite category is equivalent to the original.

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

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] :

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) :
instance CategoryTheory.isIso_unop {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X Y) [IsIso f] :
@[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

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
Instances For
@[simp]
@[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

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
@[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

The isomorphism between F.op.unop and F.

Equations

The isomorphism between F.unop.op and F.

Equations

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

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

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
Instances For
@[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

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
Instances For
@[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
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

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

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

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
@[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ᵒᵖ) :

The "unopposite" of a natural transformation.

Equations
@[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) :
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
@[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) :

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

Equations

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
@[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ᵒᵖ) :

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

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
@[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

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
def CategoryTheory.Iso.op {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (α : X Y) :

The opposite isomorphism.

Equations
  • α.op = { hom := α.hom.op, inv := α.inv.op, hom_inv_id := , inv_hom_id := }
@[simp]
theorem CategoryTheory.Iso.op_hom {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (α : X Y) :
α.op.hom = α.hom.op
@[simp]
theorem CategoryTheory.Iso.op_inv {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (α : X Y) :
α.op.inv = α.inv.op

The isomorphism obtained from an isomorphism in the opposite category.

Equations
@[simp]
theorem CategoryTheory.Iso.unop_inv {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X Y) :
@[simp]
theorem CategoryTheory.Iso.unop_hom {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X Y) :
@[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.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) :
@[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) :
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
@[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) :
@[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) :
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

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

Equations

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

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

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.

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
@[simp]
theorem CategoryTheory.opEquiv_apply {C : Type u₁} [Category.{v₁, u₁} C] (A B : Cᵒᵖ) (f : A B) :
(opEquiv A B) f = f.unop

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:

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

The equivalence of functor categories induced by op and unop.

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

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_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
@[simp]