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 : C} {Y : C} :
Function.Injective Quiver.Hom.op
theorem Quiver.Hom.unop_inj {C : Type u₁} [Quiver C] {X : Cᵒᵖ} {Y : Cᵒᵖ} :
Function.Injective Quiver.Hom.unop
@[simp]
theorem Quiver.Hom.unop_op {C : Type u₁} [Quiver C] {X : C} {Y : C} (f : X Y) :
f.op.unop = f
@[simp]
theorem Quiver.Hom.op_unop {C : Type u₁} [Quiver C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
f.unop.op = f
@[simp]
theorem CategoryTheory.op_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : Y Z} :
@[simp]
theorem CategoryTheory.unopUnop_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :
∀ {X Y : Cᵒᵖᵒᵖ} (f : X Y), (CategoryTheory.unopUnop C).map f = f.unop.unop

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

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

    The functor from a category to its double-opposite.

    Instances For

      The double opposite category is equivalent to the original.

      Instances For

        If f is an isomorphism, so is f.op

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

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

        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.

        Instances For

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

          Instances For
            @[simp]
            theorem CategoryTheory.Functor.opHom_map_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] :
            ∀ {X Y : (CategoryTheory.Functor C D)ᵒᵖ} (α : X Y) (X_1 : Cᵒᵖ), ((CategoryTheory.Functor.opHom C D).map α).app X_1 = (α.unop.app X_1.unop).op
            @[simp]
            @[simp]
            theorem CategoryTheory.Functor.leftOp_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.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.

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

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

              Instances For

                The isomorphism between F.leftOp.rightOp and F.

                Instances For

                  The isomorphism between F.rightOp.leftOp and F.

                  Instances For

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

                    The opposite of a natural transformation.

                    Instances For

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

                      Instances For

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

                        Instances For

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

                          Instances For

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

                            Instances For

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

                              Instances For

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

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

                                  The opposite isomorphism.

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

                                    The isomorphism obtained from an isomorphism in the opposite category.

                                    Instances For

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

                                      Instances For

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

                                        Instances For

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

                                          Instances For

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

                                            Instances For

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

                                              Instances For
                                                @[simp]
                                                theorem CategoryTheory.opEquiv_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Cᵒᵖ) (B : Cᵒᵖ) (f : A B) :
                                                ↑(CategoryTheory.opEquiv A B) f = f.unop
                                                @[simp]
                                                theorem CategoryTheory.opEquiv_symm_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Cᵒᵖ) (B : Cᵒᵖ) (g : B.unop A.unop) :
                                                (CategoryTheory.opEquiv A B).symm g = g.op
                                                def CategoryTheory.opEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Cᵒᵖ) (B : Cᵒᵖ) :
                                                (A B) (B.unop A.unop)

                                                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 _ _
                                                
                                                Instances For
                                                  def CategoryTheory.isoOpEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Cᵒᵖ) (B : Cᵒᵖ) :
                                                  (A B) (B.unop A.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:

                                                  Instances For