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

The opposite category.

See .

Equations
@[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
        • F.op = { toPrefunctor := { obj := fun (X : Cᵒᵖ) => Opposite.op (F.obj X.unop), map := fun {X Y : Cᵒᵖ} (f : X Y) => (F.map f.unop).op }, map_id := , map_comp := }
        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.

          Equations
          • One or more equations did not get rendered due to their size.
          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

            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 α = { app := fun (X_1 : C) => (α.app (Opposite.op X_1)).unop, naturality := }.op

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

                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 = { toPrefunctor := { obj := fun (X : Cᵒᵖ) => (F.obj X.unop).unop, map := fun {X Y : Cᵒᵖ} (f : X Y) => (F.map f.unop).unop }, map_id := , map_comp := }
                Instances For
                  @[simp]
                  theorem CategoryTheory.Functor.rightOp_map {C : Type u₁} [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
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    • CategoryTheory.Functor.instFullOppositeOppositeOppositeOppositeOp = { preimage := fun (X Y : Cᵒᵖ) (f : F.op.obj X F.op.obj Y) => (F.preimage f.unop).op, witness := }

                    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) :
                                        (CategoryTheory.Iso.op α).hom = α.hom.op
                                        @[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

                                        The opposite isomorphism.

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

                                          Equations
                                          Instances For

                                            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

                                                  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]
                                                      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
                                                      @[simp]
                                                      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 _ _
                                                      
                                                      Equations
                                                      • CategoryTheory.opEquiv A B = { toFun := fun (f : A B) => f.unop, invFun := fun (g : B.unop A.unop) => g.op, left_inv := , right_inv := }
                                                      Instances For
                                                        Equations
                                                        • =
                                                        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:

                                                        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