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.

source
theorem Quiver.Hom.op_inj {C : Type u₁} [Quiver C] {X : C} {Y : C} :
Function.Injective Quiver.Hom.op
source
theorem Quiver.Hom.unop_inj {C : Type u₁} [Quiver C] {X : Cᵒᵖ} {Y : Cᵒᵖ} :
Function.Injective Quiver.Hom.unop
source
@[simp]
theorem Quiver.Hom.unop_op {C : Type u₁} [Quiver C] {X : C} {Y : C} (f : X ⟶ Y) :
f.op.unop = f
source
@[simp]
theorem Quiver.Hom.op_unop {C : Type u₁} [Quiver C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ⟶ Y) :
f.unop.op = f
source
instance CategoryTheory.Category.opposite {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
CategoryTheory.Category.{v₁, u₁} Cᵒᵖ

The opposite category.

See https://stacks.math.columbia.edu/tag/001M.

source
theorem CategoryTheory.op_comp_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {Z : Cᵒᵖ} (h : Opposite.op X ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).op h = CategoryTheory.CategoryStruct.comp g.op (CategoryTheory.CategoryStruct.comp f.op h)
source
@[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} :
(CategoryTheory.CategoryStruct.comp f g).op = CategoryTheory.CategoryStruct.comp g.op f.op
source
@[simp]
theorem CategoryTheory.op_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} :
(CategoryTheory.CategoryStruct.id X).op = CategoryTheory.CategoryStruct.id (Opposite.op X)
source
theorem CategoryTheory.unop_comp_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} {Z : C} (h : X.unop ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).unop h = CategoryTheory.CategoryStruct.comp g.unop (CategoryTheory.CategoryStruct.comp f.unop h)
source
@[simp]
theorem CategoryTheory.unop_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} :
(CategoryTheory.CategoryStruct.comp f g).unop = CategoryTheory.CategoryStruct.comp g.unop f.unop
source
@[simp]
theorem CategoryTheory.unop_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} :
(CategoryTheory.CategoryStruct.id X).unop = CategoryTheory.CategoryStruct.id X.unop
source
@[simp]
theorem CategoryTheory.unop_id_op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} :
(CategoryTheory.CategoryStruct.id (Opposite.op X)).unop = CategoryTheory.CategoryStruct.id X
source
@[simp]
theorem CategoryTheory.op_id_unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} :
(CategoryTheory.CategoryStruct.id X.unop).op = CategoryTheory.CategoryStruct.id X
source
@[simp]
theorem CategoryTheory.unopUnop_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖᵒᵖ) :
(CategoryTheory.unopUnop C).obj X = X.unop.unop
source
@[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
source
def CategoryTheory.unopUnop (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :
CategoryTheory.Functor Cᵒᵖᵒᵖ C

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

Instances For
    source
    @[simp]
    theorem CategoryTheory.opOp_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) :
    (CategoryTheory.opOp C).obj X = Opposite.op (Opposite.op X)
    source
    @[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
    source
    def CategoryTheory.opOp (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :
    CategoryTheory.Functor C Cᵒᵖᵒᵖ

    The functor from a category to its double-opposite.

    Instances For
      source
      @[simp]
      theorem CategoryTheory.opOpEquivalence_functor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :
      (CategoryTheory.opOpEquivalence C).functor = CategoryTheory.unopUnop C
      source
      @[simp]
      theorem CategoryTheory.opOpEquivalence_unitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :
      (CategoryTheory.opOpEquivalence C).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id Cᵒᵖᵒᵖ)
      source
      @[simp]
      theorem CategoryTheory.opOpEquivalence_inverse (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :
      (CategoryTheory.opOpEquivalence C).inverse = CategoryTheory.opOp C
      source
      @[simp]
      theorem CategoryTheory.opOpEquivalence_counitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :
      (CategoryTheory.opOpEquivalence C).counitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.comp (CategoryTheory.opOp C) (CategoryTheory.unopUnop C))
      source
      def CategoryTheory.opOpEquivalence (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :
      Cᵒᵖᵒᵖ ≌ C

      The double opposite category is equivalent to the original.

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

        If f is an isomorphism, so is f.op

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

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

        source
        theorem CategoryTheory.isIso_op_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) :
        CategoryTheory.IsIso f.op ↔ CategoryTheory.IsIso f
        source
        theorem CategoryTheory.isIso_unop_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ⟶ Y) :
        CategoryTheory.IsIso f.unop ↔ CategoryTheory.IsIso f
        source
        instance CategoryTheory.isIso_unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ⟶ Y) [CategoryTheory.IsIso f] :
        CategoryTheory.IsIso f.unop
        source
        @[simp]
        theorem CategoryTheory.op_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] :
        (CategoryTheory.inv f).op = CategoryTheory.inv f.op
        source
        @[simp]
        theorem CategoryTheory.unop_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ⟶ Y) [CategoryTheory.IsIso f] :
        (CategoryTheory.inv f).unop = CategoryTheory.inv f.unop
        source
        @[simp]
        theorem CategoryTheory.Functor.op_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : Cᵒᵖ) :
        F.op.obj X = Opposite.op (F.obj X.unop)
        source
        @[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
        source
        def CategoryTheory.Functor.op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
        CategoryTheory.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.

        Instances For
          source
          @[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), (CategoryTheory.Functor.unop F).map f = (F.map f.op).unop
          source
          @[simp]
          theorem CategoryTheory.Functor.unop_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (X : C) :
          (CategoryTheory.Functor.unop F).obj X = (F.obj (Opposite.op X)).unop
          source
          def CategoryTheory.Functor.unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) :
          CategoryTheory.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.

          Instances For
            source
            @[simp]
            theorem CategoryTheory.Functor.opUnopIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) :
            (CategoryTheory.Functor.opUnopIso F).hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
            source
            @[simp]
            theorem CategoryTheory.Functor.opUnopIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) :
            (CategoryTheory.Functor.opUnopIso F).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
            source
            def CategoryTheory.Functor.opUnopIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
            CategoryTheory.Functor.unop F.op ≅ F

            The isomorphism between F.op.unop and F.

            Instances For
              source
              @[simp]
              theorem CategoryTheory.Functor.unopOpIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (X : Cᵒᵖ) :
              (CategoryTheory.Functor.unopOpIso F).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
              source
              @[simp]
              theorem CategoryTheory.Functor.unopOpIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (X : Cᵒᵖ) :
              (CategoryTheory.Functor.unopOpIso F).hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
              source
              def CategoryTheory.Functor.unopOpIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) :
              (CategoryTheory.Functor.unop F).op ≅ F

              The isomorphism between F.unop.op and F.

              Instances For
                source
                @[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
                source
                @[simp]
                theorem CategoryTheory.Functor.opHom_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (F : (CategoryTheory.Functor C D)ᵒᵖ) :
                (CategoryTheory.Functor.opHom C D).obj F = F.unop.op
                source
                def CategoryTheory.Functor.opHom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] :
                CategoryTheory.Functor (CategoryTheory.Functor C D)ᵒᵖ (CategoryTheory.Functor Cᵒᵖ Dᵒᵖ)

                Taking the opposite of a functor is functorial.

                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.opInv_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) :
                  (CategoryTheory.Functor.opInv C D).obj F = Opposite.op (CategoryTheory.Functor.unop F)
                  source
                  @[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 α = (CategoryTheory.NatTrans.mk fun X_1 => (α.app (Opposite.op X_1)).unop).op
                  source
                  def CategoryTheory.Functor.opInv (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] :
                  CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (CategoryTheory.Functor C D)ᵒᵖ

                  Take the "unopposite" of a functor is functorial.

                  Instances For
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.leftOp_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) (X : Cᵒᵖ) :
                    F.leftOp.obj X = (F.obj X.unop).unop
                    source
                    @[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
                    source
                    def CategoryTheory.Functor.leftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) :
                    CategoryTheory.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.

                    Instances For
                      source
                      @[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
                      source
                      @[simp]
                      theorem CategoryTheory.Functor.rightOp_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) (X : C) :
                      F.rightOp.obj X = Opposite.op (F.obj (Opposite.op X))
                      source
                      def CategoryTheory.Functor.rightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) :
                      CategoryTheory.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.

                      Instances For
                        source
                        instance CategoryTheory.Functor.instFullOppositeOppositeOppositeOppositeOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [CategoryTheory.Full F] :
                        CategoryTheory.Full F.op
                        source
                        instance CategoryTheory.Functor.instFaithfulOppositeOppositeOppositeOppositeOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [CategoryTheory.Faithful F] :
                        CategoryTheory.Faithful F.op
                        source
                        instance CategoryTheory.Functor.rightOp_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} [CategoryTheory.Faithful F] :
                        CategoryTheory.Faithful F.rightOp

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

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

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

                        source
                        @[simp]
                        theorem CategoryTheory.Functor.leftOpRightOpIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) (X : C) :
                        (CategoryTheory.Functor.leftOpRightOpIso F).hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
                        source
                        @[simp]
                        theorem CategoryTheory.Functor.leftOpRightOpIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) (X : C) :
                        (CategoryTheory.Functor.leftOpRightOpIso F).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
                        source
                        def CategoryTheory.Functor.leftOpRightOpIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) :
                        F.leftOp.rightOp ≅ F

                        The isomorphism between F.leftOp.rightOp and F.

                        Instances For
                          source
                          @[simp]
                          theorem CategoryTheory.Functor.rightOpLeftOpIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) (X : Cᵒᵖ) :
                          (CategoryTheory.Functor.rightOpLeftOpIso F).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
                          source
                          @[simp]
                          theorem CategoryTheory.Functor.rightOpLeftOpIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) (X : Cᵒᵖ) :
                          (CategoryTheory.Functor.rightOpLeftOpIso F).hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
                          source
                          def CategoryTheory.Functor.rightOpLeftOpIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) :
                          F.rightOp.leftOp ≅ F

                          The isomorphism between F.rightOp.leftOp and F.

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

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

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

                            The opposite of a natural transformation.

                            Instances For
                              source
                              @[simp]
                              theorem CategoryTheory.NatTrans.op_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
                              CategoryTheory.NatTrans.op (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.op
                              source
                              @[simp]
                              theorem CategoryTheory.NatTrans.unop_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : F ⟶ G) (X : C) :
                              (CategoryTheory.NatTrans.unop α).app X = (α.app (Opposite.op X)).unop
                              source
                              def CategoryTheory.NatTrans.unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : F ⟶ G) :
                              CategoryTheory.Functor.unop G ⟶ CategoryTheory.Functor.unop F

                              The "unopposite" of a natural transformation.

                              Instances For
                                source
                                @[simp]
                                theorem CategoryTheory.NatTrans.unop_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) :
                                CategoryTheory.NatTrans.unop (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.unop F)
                                source
                                @[simp]
                                theorem CategoryTheory.NatTrans.removeOp_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F.op ⟶ G.op) (X : C) :
                                (CategoryTheory.NatTrans.removeOp α).app X = (α.app (Opposite.op X)).unop
                                source
                                def CategoryTheory.NatTrans.removeOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.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.

                                Instances For
                                  source
                                  @[simp]
                                  theorem CategoryTheory.NatTrans.removeOp_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
                                  CategoryTheory.NatTrans.removeOp (CategoryTheory.CategoryStruct.id F.op) = CategoryTheory.CategoryStruct.id F
                                  source
                                  @[simp]
                                  theorem CategoryTheory.NatTrans.removeUnop_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : CategoryTheory.Functor.unop F ⟶ CategoryTheory.Functor.unop G) (X : Cᵒᵖ) :
                                  (CategoryTheory.NatTrans.removeUnop α).app X = (α.app X.unop).op
                                  source
                                  def CategoryTheory.NatTrans.removeUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : CategoryTheory.Functor.unop F ⟶ CategoryTheory.Functor.unop G) :
                                  G ⟶ F

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

                                  Instances For
                                    source
                                    @[simp]
                                    theorem CategoryTheory.NatTrans.removeUnop_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) :
                                    CategoryTheory.NatTrans.removeUnop (CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.unop F)) = CategoryTheory.CategoryStruct.id F
                                    source
                                    @[simp]
                                    theorem CategoryTheory.NatTrans.leftOp_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C Dᵒᵖ} {G : CategoryTheory.Functor C Dᵒᵖ} (α : F ⟶ G) (X : Cᵒᵖ) :
                                    (CategoryTheory.NatTrans.leftOp α).app X = (α.app X.unop).unop
                                    source
                                    def CategoryTheory.NatTrans.leftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C Dᵒᵖ} {G : CategoryTheory.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.

                                    Instances For
                                      source
                                      @[simp]
                                      theorem CategoryTheory.NatTrans.leftOp_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C Dᵒᵖ} :
                                      CategoryTheory.NatTrans.leftOp (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.leftOp
                                      source
                                      @[simp]
                                      theorem CategoryTheory.NatTrans.leftOp_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C Dᵒᵖ} {G : CategoryTheory.Functor C Dᵒᵖ} {H : CategoryTheory.Functor C Dᵒᵖ} (α : F ⟶ G) (β : G ⟶ H) :
                                      CategoryTheory.NatTrans.leftOp (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftOp β) (CategoryTheory.NatTrans.leftOp α)
                                      source
                                      @[simp]
                                      theorem CategoryTheory.NatTrans.removeLeftOp_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C Dᵒᵖ} {G : CategoryTheory.Functor C Dᵒᵖ} (α : F.leftOp ⟶ G.leftOp) (X : C) :
                                      (CategoryTheory.NatTrans.removeLeftOp α).app X = (α.app (Opposite.op X)).op
                                      source
                                      def CategoryTheory.NatTrans.removeLeftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C Dᵒᵖ} {G : CategoryTheory.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.

                                      Instances For
                                        source
                                        @[simp]
                                        theorem CategoryTheory.NatTrans.removeLeftOp_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C Dᵒᵖ} :
                                        CategoryTheory.NatTrans.removeLeftOp (CategoryTheory.CategoryStruct.id F.leftOp) = CategoryTheory.CategoryStruct.id F
                                        source
                                        @[simp]
                                        theorem CategoryTheory.NatTrans.rightOp_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} {G : CategoryTheory.Functor Cᵒᵖ D} (α : F ⟶ G) (X : C) :
                                        (CategoryTheory.NatTrans.rightOp α).app X = (α.app (Opposite.op X)).op
                                        source
                                        def CategoryTheory.NatTrans.rightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} {G : CategoryTheory.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.

                                        Instances For
                                          source
                                          @[simp]
                                          theorem CategoryTheory.NatTrans.rightOp_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} :
                                          CategoryTheory.NatTrans.rightOp (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.rightOp
                                          source
                                          @[simp]
                                          theorem CategoryTheory.NatTrans.rightOp_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} {G : CategoryTheory.Functor Cᵒᵖ D} {H : CategoryTheory.Functor Cᵒᵖ D} (α : F ⟶ G) (β : G ⟶ H) :
                                          CategoryTheory.NatTrans.rightOp (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightOp β) (CategoryTheory.NatTrans.rightOp α)
                                          source
                                          @[simp]
                                          theorem CategoryTheory.NatTrans.removeRightOp_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} {G : CategoryTheory.Functor Cᵒᵖ D} (α : F.rightOp ⟶ G.rightOp) (X : Cᵒᵖ) :
                                          (CategoryTheory.NatTrans.removeRightOp α).app X = (α.app X.unop).unop
                                          source
                                          def CategoryTheory.NatTrans.removeRightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} {G : CategoryTheory.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.

                                          Instances For
                                            source
                                            @[simp]
                                            theorem CategoryTheory.NatTrans.removeRightOp_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} :
                                            CategoryTheory.NatTrans.removeRightOp (CategoryTheory.CategoryStruct.id F.rightOp) = CategoryTheory.CategoryStruct.id F
                                            source
                                            @[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
                                            source
                                            @[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
                                            source
                                            def CategoryTheory.Iso.op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (α : X ≅ Y) :
                                            Opposite.op Y ≅ Opposite.op X

                                            The opposite isomorphism.

                                            Instances For
                                              source
                                              @[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
                                              source
                                              @[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
                                              source
                                              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
                                                source
                                                @[simp]
                                                theorem CategoryTheory.Iso.unop_op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ≅ Y) :
                                                CategoryTheory.Iso.op (CategoryTheory.Iso.unop f) = f
                                                source
                                                @[simp]
                                                theorem CategoryTheory.Iso.op_unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ≅ Y) :
                                                CategoryTheory.Iso.unop (CategoryTheory.Iso.op f) = f
                                                source
                                                @[simp]
                                                theorem CategoryTheory.NatIso.op_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F ≅ G) :
                                                (CategoryTheory.NatIso.op α).inv = CategoryTheory.NatTrans.op α.inv
                                                source
                                                @[simp]
                                                theorem CategoryTheory.NatIso.op_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F ≅ G) :
                                                (CategoryTheory.NatIso.op α).hom = CategoryTheory.NatTrans.op α.hom
                                                source
                                                def CategoryTheory.NatIso.op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.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.

                                                Instances For
                                                  source
                                                  @[simp]
                                                  theorem CategoryTheory.NatIso.removeOp_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F.op ≅ G.op) :
                                                  (CategoryTheory.NatIso.removeOp α).inv = CategoryTheory.NatTrans.removeOp α.inv
                                                  source
                                                  @[simp]
                                                  theorem CategoryTheory.NatIso.removeOp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F.op ≅ G.op) :
                                                  (CategoryTheory.NatIso.removeOp α).hom = CategoryTheory.NatTrans.removeOp α.hom
                                                  source
                                                  def CategoryTheory.NatIso.removeOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.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.

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

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

                                                    Instances For
                                                      source
                                                      @[simp]
                                                      theorem CategoryTheory.Equivalence.op_counitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :
                                                      (CategoryTheory.Equivalence.op e).counitIso = (CategoryTheory.NatIso.op e.counitIso).symm
                                                      source
                                                      @[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) :
                                                      (CategoryTheory.Equivalence.op e).functor = e.functor.op
                                                      source
                                                      @[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) :
                                                      (CategoryTheory.Equivalence.op e).inverse = e.inverse.op
                                                      source
                                                      @[simp]
                                                      theorem CategoryTheory.Equivalence.op_unitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :
                                                      (CategoryTheory.Equivalence.op e).unitIso = (CategoryTheory.NatIso.op e.unitIso).symm
                                                      source
                                                      def CategoryTheory.Equivalence.op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :
                                                      Cᵒᵖ ≌ Dᵒᵖ

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

                                                      Instances For
                                                        source
                                                        @[simp]
                                                        theorem CategoryTheory.Equivalence.unop_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ Dᵒᵖ) :
                                                        (CategoryTheory.Equivalence.unop e).inverse = CategoryTheory.Functor.unop e.inverse
                                                        source
                                                        @[simp]
                                                        theorem CategoryTheory.Equivalence.unop_unitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ Dᵒᵖ) :
                                                        (CategoryTheory.Equivalence.unop e).unitIso = (CategoryTheory.NatIso.unop e.unitIso).symm
                                                        source
                                                        @[simp]
                                                        theorem CategoryTheory.Equivalence.unop_counitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ Dᵒᵖ) :
                                                        (CategoryTheory.Equivalence.unop e).counitIso = (CategoryTheory.NatIso.unop e.counitIso).symm
                                                        source
                                                        @[simp]
                                                        theorem CategoryTheory.Equivalence.unop_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ Dᵒᵖ) :
                                                        (CategoryTheory.Equivalence.unop e).functor = CategoryTheory.Functor.unop e.functor
                                                        source
                                                        def CategoryTheory.Equivalence.unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ Dᵒᵖ) :
                                                        C ≌ D

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

                                                        Instances For
                                                          source
                                                          @[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
                                                          source
                                                          @[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
                                                          source
                                                          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
                                                            source
                                                            instance CategoryTheory.subsingleton_of_unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Cᵒᵖ) (B : Cᵒᵖ) [Subsingleton (B.unop ⟶ A.unop)] :
                                                            Subsingleton (A ⟶ B)
                                                            source
                                                            instance CategoryTheory.decidableEqOfUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Cᵒᵖ) (B : Cᵒᵖ) [DecidableEq (B.unop ⟶ A.unop)] :
                                                            DecidableEq (A ⟶ B)
                                                            source
                                                            @[simp]
                                                            theorem CategoryTheory.isoOpEquiv_symm_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Cᵒᵖ) (B : Cᵒᵖ) (g : B.unop ≅ A.unop) :
                                                            ↑(CategoryTheory.isoOpEquiv A B).symm g = CategoryTheory.Iso.op g
                                                            source
                                                            @[simp]
                                                            theorem CategoryTheory.isoOpEquiv_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Cᵒᵖ) (B : Cᵒᵖ) (f : A ≅ B) :
                                                            ↑(CategoryTheory.isoOpEquiv A B) f = CategoryTheory.Iso.unop f
                                                            source
                                                            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
                                                              source
                                                              @[simp]
                                                              theorem CategoryTheory.Functor.opUnopEquiv_functor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] :
                                                              (CategoryTheory.Functor.opUnopEquiv C D).functor = CategoryTheory.Functor.opHom C D
                                                              source
                                                              @[simp]
                                                              theorem CategoryTheory.Functor.opUnopEquiv_unitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] :
                                                              (CategoryTheory.Functor.opUnopEquiv C D).unitIso = CategoryTheory.NatIso.ofComponents fun F => CategoryTheory.Iso.op (CategoryTheory.Functor.opUnopIso F.unop)
                                                              source
                                                              @[simp]
                                                              theorem CategoryTheory.Functor.opUnopEquiv_counitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] :
                                                              (CategoryTheory.Functor.opUnopEquiv C D).counitIso = CategoryTheory.NatIso.ofComponents fun F => CategoryTheory.Functor.unopOpIso F
                                                              source
                                                              @[simp]
                                                              theorem CategoryTheory.Functor.opUnopEquiv_inverse (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] :
                                                              (CategoryTheory.Functor.opUnopEquiv C D).inverse = CategoryTheory.Functor.opInv C D
                                                              source
                                                              def CategoryTheory.Functor.opUnopEquiv (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] :
                                                              (CategoryTheory.Functor C D)ᵒᵖ ≌ CategoryTheory.Functor Cᵒᵖ Dᵒᵖ

                                                              The equivalence of functor categories induced by op and unop.

                                                              Instances For
                                                                source
                                                                @[simp]
                                                                theorem CategoryTheory.Functor.leftOpRightOpEquiv_functor_obj_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), ((CategoryTheory.Functor.leftOpRightOpEquiv C D).functor.obj F).map f = (F.unop.map f.op).op
                                                                source
                                                                @[simp]
                                                                theorem CategoryTheory.Functor.leftOpRightOpEquiv_functor_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.leftOpRightOpEquiv C D).functor.map η).app X_1 = (η.unop.app (Opposite.op X_1)).op
                                                                source
                                                                @[simp]
                                                                theorem CategoryTheory.Functor.leftOpRightOpEquiv_counitIso_inv_app_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : CategoryTheory.Functor C Dᵒᵖ) (X : C) :
                                                                ((CategoryTheory.Functor.leftOpRightOpEquiv C D).counitIso.inv.app X).app X = CategoryTheory.CategoryStruct.id (X.obj X)
                                                                source
                                                                @[simp]
                                                                theorem CategoryTheory.Functor.leftOpRightOpEquiv_unitIso_inv_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ) :
                                                                (CategoryTheory.Functor.leftOpRightOpEquiv C D).unitIso.inv.app X = (CategoryTheory.Functor.rightOpLeftOpIso X.unop).inv.op
                                                                source
                                                                @[simp]
                                                                theorem CategoryTheory.Functor.leftOpRightOpEquiv_counitIso_hom_app_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : CategoryTheory.Functor C Dᵒᵖ) (X : C) :
                                                                ((CategoryTheory.Functor.leftOpRightOpEquiv C D).counitIso.hom.app X).app X = CategoryTheory.CategoryStruct.id (X.obj X)
                                                                source
                                                                @[simp]
                                                                theorem CategoryTheory.Functor.leftOpRightOpEquiv_unitIso_hom_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ) :
                                                                (CategoryTheory.Functor.leftOpRightOpEquiv C D).unitIso.hom.app X = (CategoryTheory.Functor.rightOpLeftOpIso X.unop).hom.op
                                                                source
                                                                @[simp]
                                                                theorem CategoryTheory.Functor.leftOpRightOpEquiv_inverse_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) :
                                                                (CategoryTheory.Functor.leftOpRightOpEquiv C D).inverse.obj F = Opposite.op F.leftOp
                                                                source
                                                                @[simp]
                                                                theorem CategoryTheory.Functor.leftOpRightOpEquiv_functor_obj_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (F : (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ) (X : C) :
                                                                ((CategoryTheory.Functor.leftOpRightOpEquiv C D).functor.obj F).obj X = Opposite.op (F.unop.obj (Opposite.op X))
                                                                source
                                                                @[simp]
                                                                theorem CategoryTheory.Functor.leftOpRightOpEquiv_inverse_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.leftOpRightOpEquiv C D).inverse.map η = (CategoryTheory.NatTrans.leftOp η).op
                                                                source
                                                                def CategoryTheory.Functor.leftOpRightOpEquiv (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] :
                                                                (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ ≌ CategoryTheory.Functor C Dᵒᵖ

                                                                The equivalence of functor categories induced by leftOp and rightOp.

                                                                Instances For