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]
@[simp]
theorem Quiver.Hom.op_unop {C : Type u₁} [Quiver C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
f.unop.op = f
@[simp]
theorem Quiver.Hom.unop_mk {C : Type u₁} [Quiver C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
@[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.

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

    Equations
    Instances For

      The double opposite category is equivalent to the original.

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

        If f is an isomorphism, so is f.op

        Equations
        • =

        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.

        Equations
        Instances For
          @[simp]
          theorem CategoryTheory.Functor.unop_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.unop.map f = (F.map f.op).unop

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

            The isomorphism between F.op.unop and F.

            Equations
            Instances For

              The isomorphism between F.unop.op and F.

              Equations
              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 (Opposite.unop X_1)).op

                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₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] :
                  ∀ {X Y : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : X Y), (CategoryTheory.Functor.opInv C D).map α = Quiver.Hom.op { app := fun (X_1 : C) => (α.app (Opposite.op X_1)).unop, naturality := }

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

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

                      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 := }
                      Instances For
                        theorem CategoryTheory.Functor.rightOp_map_unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} {X : C} {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.

                        Equations
                        • =

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

                        Equations
                        • =

                        The isomorphism between F.leftOp.rightOp and F.

                        Equations
                        Instances For

                          The isomorphism between F.rightOp.leftOp and F.

                          Equations
                          Instances For

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

                            The opposite of a natural transformation.

                            Equations
                            Instances For

                              The "unopposite" of a natural transformation.

                              Equations
                              Instances For

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

                                Equations
                                Instances For

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

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

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

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

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

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

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

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

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

                                                Equations
                                                Instances For

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

                                                  Equations
                                                  Instances For

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

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem CategoryTheory.Equivalence.op_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) :
                                                      e.op.functor = e.functor.op
                                                      @[simp]
                                                      theorem CategoryTheory.Equivalence.op_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) :
                                                      e.op.inverse = e.inverse.op

                                                      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

                                                        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]

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

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

                                                              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

                                                                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
                                                                  Equations
                                                                  • =
                                                                  Equations
                                                                  • =
                                                                  Equations
                                                                  • =