Documentation

Mathlib.CategoryTheory.Monoidal.Opposite

Monoidal opposites #

We write Cᵐᵒᵖ for the monoidal opposite of a monoidal category C.

source
structure CategoryTheory.MonoidalOpposite (C : Type u₁) :
Type u₁

The type of objects of the opposite (or "reverse") monoidal category. Use the notation Cᴹᵒᵖ.

Instances For
    source
    def CategoryTheory.MonoidalOpposite.«term_ᴹᵒᵖ» :
    Lean.TrailingParserDescr

    The type of objects of the opposite (or "reverse") monoidal category. Use the notation Cᴹᵒᵖ.

    Equations
    Instances For
      source
      theorem CategoryTheory.MonoidalOpposite.mop_injective {C : Type u₁} :
      Function.Injective mop
      source
      theorem CategoryTheory.MonoidalOpposite.unmop_injective {C : Type u₁} :
      Function.Injective unmop
      source
      theorem CategoryTheory.MonoidalOpposite.mop_inj_iff {C : Type u₁} (x y : C) :
      { unmop := x } = { unmop := y } ↔ x = y
      source
      @[simp]
      theorem CategoryTheory.MonoidalOpposite.unmop_inj_iff {C : Type u₁} (x y : Cᴹᵒᵖ) :
      x.unmop = y.unmop ↔ x = y
      source
      @[simp]
      theorem CategoryTheory.MonoidalOpposite.mop_unmop {C : Type u₁} (X : Cᴹᵒᵖ) :
      { unmop := X.unmop } = X
      source
      theorem CategoryTheory.MonoidalOpposite.unmop_mop {C : Type u₁} (X : C) :
      { unmop := X }.unmop = X
      source
      instance CategoryTheory.MonoidalOpposite.monoidalOppositeCategory {C : Type u₁} [Category.{v₁, u₁} C] :
      Category.{v₁, u₁} Cᴹᵒᵖ
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Quiver.Hom.mop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :
      { unmop := X } ⟶ { unmop := Y }

      The monoidal opposite of a morphism f : X ⟶ Y is just f, thought of as mop X ⟶ mop Y.

      Equations
      Instances For
        source
        def Quiver.Hom.unmop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᴹᵒᵖ} (f : X ⟶ Y) :
        X.unmop ⟶ Y.unmop

        We can think of a morphism f : mop X ⟶ mop Y as a morphism X ⟶ Y.

        Equations
        Instances For
          source
          theorem Quiver.Hom.mop_inj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} :
          Function.Injective mop
          source
          theorem Quiver.Hom.unmop_inj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᴹᵒᵖ} :
          Function.Injective unmop
          source
          @[simp]
          theorem Quiver.Hom.unmop_mop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} :
          f.mop.unmop = f
          source
          @[simp]
          theorem Quiver.Hom.mop_unmop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᴹᵒᵖ} {f : X ⟶ Y} :
          f.unmop.mop = f
          source
          @[simp]
          theorem CategoryTheory.mop_comp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} :
          (CategoryStruct.comp f g).mop = CategoryStruct.comp f.mop g.mop
          source
          @[simp]
          theorem CategoryTheory.mop_id {C : Type u₁} [Category.{v₁, u₁} C] {X : C} :
          (CategoryStruct.id X).mop = CategoryStruct.id { unmop := X }
          source
          @[simp]
          theorem CategoryTheory.unmop_comp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᴹᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} :
          (CategoryStruct.comp f g).unmop = CategoryStruct.comp f.unmop g.unmop
          source
          @[simp]
          theorem CategoryTheory.unmop_id {C : Type u₁} [Category.{v₁, u₁} C] {X : Cᴹᵒᵖ} :
          (CategoryStruct.id X).unmop = CategoryStruct.id X.unmop
          source
          @[simp]
          theorem CategoryTheory.unmop_id_mop {C : Type u₁} [Category.{v₁, u₁} C] {X : C} :
          (CategoryStruct.id { unmop := X }).unmop = CategoryStruct.id X
          source
          @[simp]
          theorem CategoryTheory.mop_id_unmop {C : Type u₁} [Category.{v₁, u₁} C] {X : Cᴹᵒᵖ} :
          (CategoryStruct.id X.unmop).mop = CategoryStruct.id X
          source
          def CategoryTheory.mopFunctor (C : Type u₁) [Category.{v₁, u₁} C] :
          Functor C Cᴹᵒᵖ

          The identity functor on C, viewed as a functor from C to its monoidal opposite.

          Equations
          Instances For
            source
            @[simp]
            theorem CategoryTheory.mopFunctor_map (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
            (mopFunctor C).map f = f.mop
            source
            @[simp]
            theorem CategoryTheory.mopFunctor_obj (C : Type u₁) [Category.{v₁, u₁} C] (unmop : C) :
            (mopFunctor C).obj unmop = { unmop := unmop }
            source
            def CategoryTheory.unmopFunctor (C : Type u₁) [Category.{v₁, u₁} C] :
            Functor Cᴹᵒᵖ C

            The identity functor on C, viewed as a functor from the monoidal opposite of C to C.

            Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.unmopFunctor_obj (C : Type u₁) [Category.{v₁, u₁} C] (self : Cᴹᵒᵖ) :
              (unmopFunctor C).obj self = self.unmop
              source
              @[simp]
              theorem CategoryTheory.unmopFunctor_map (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : Cᴹᵒᵖ} (f : X✝ ⟶ Y✝) :
              (unmopFunctor C).map f = f.unmop
              source
              @[reducible, inline]
              abbrev CategoryTheory.Iso.mop {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ≅ Y) :
              { unmop := X } ≅ { unmop := Y }

              An isomorphism in C gives an isomorphism in Cᴹᵒᵖ.

              Equations
              Instances For
                source
                @[reducible, inline]
                abbrev CategoryTheory.Iso.unmop {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᴹᵒᵖ} (f : X ≅ Y) :
                X.unmop ≅ Y.unmop

                An isomorphism in Cᴹᵒᵖ gives an isomorphism in C.

                Equations
                Instances For
                  source
                  instance CategoryTheory.IsIso.instMonoidalOppositeMop {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsIso f] :
                  IsIso f.mop
                  source
                  instance CategoryTheory.IsIso.instUnmopOfMonoidalOpposite {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᴹᵒᵖ} (f : X ⟶ Y) [IsIso f] :
                  IsIso f.unmop
                  source
                  instance CategoryTheory.monoidalCategoryOp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :
                  MonoidalCategory Cᵒᵖ
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  @[simp]
                  theorem CategoryTheory.op_tensorObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : C) :
                  Opposite.op (MonoidalCategoryStruct.tensorObj X Y) = MonoidalCategoryStruct.tensorObj (Opposite.op X) (Opposite.op Y)
                  source
                  @[simp]
                  theorem CategoryTheory.unop_tensorObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : Cᵒᵖ) :
                  Opposite.unop (MonoidalCategoryStruct.tensorObj X Y) = MonoidalCategoryStruct.tensorObj (Opposite.unop X) (Opposite.unop Y)
                  source
                  @[simp]
                  theorem CategoryTheory.op_tensorUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :
                  Opposite.op (MonoidalCategoryStruct.tensorUnit C) = MonoidalCategoryStruct.tensorUnit Cᵒᵖ
                  source
                  @[simp]
                  theorem CategoryTheory.unop_tensorUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :
                  Opposite.unop (MonoidalCategoryStruct.tensorUnit Cᵒᵖ) = MonoidalCategoryStruct.tensorUnit C
                  source
                  @[simp]
                  theorem CategoryTheory.op_tensorHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
                  (MonoidalCategoryStruct.tensorHom f g).op = MonoidalCategoryStruct.tensorHom f.op g.op
                  source
                  @[simp]
                  theorem CategoryTheory.unop_tensorHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X₁ Y₁ X₂ Y₂ : Cᵒᵖ} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
                  (MonoidalCategoryStruct.tensorHom f g).unop = MonoidalCategoryStruct.tensorHom f.unop g.unop
                  source
                  @[simp]
                  theorem CategoryTheory.op_whiskerLeft {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z) :
                  (MonoidalCategoryStruct.whiskerLeft X f).op = MonoidalCategoryStruct.whiskerLeft (Opposite.op X) f.op
                  source
                  @[simp]
                  theorem CategoryTheory.unop_whiskerLeft {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᵒᵖ) {Y Z : Cᵒᵖ} (f : Y ⟶ Z) :
                  (MonoidalCategoryStruct.whiskerLeft X f).unop = MonoidalCategoryStruct.whiskerLeft (Opposite.unop X) f.unop
                  source
                  @[simp]
                  theorem CategoryTheory.op_whiskerRight {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : C} (f : X ⟶ Y) (Z : C) :
                  (MonoidalCategoryStruct.whiskerRight f Z).op = MonoidalCategoryStruct.whiskerRight f.op (Opposite.op Z)
                  source
                  @[simp]
                  theorem CategoryTheory.unop_whiskerRight {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : Cᵒᵖ} (f : X ⟶ Y) (Z : Cᵒᵖ) :
                  (MonoidalCategoryStruct.whiskerRight f Z).unop = MonoidalCategoryStruct.whiskerRight f.unop (Opposite.unop Z)
                  source
                  @[simp]
                  theorem CategoryTheory.op_associator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y Z : C) :
                  (MonoidalCategoryStruct.associator X Y Z).op = (MonoidalCategoryStruct.associator (Opposite.op X) (Opposite.op Y) (Opposite.op Z)).symm
                  source
                  @[simp]
                  theorem CategoryTheory.unop_associator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y Z : Cᵒᵖ) :
                  (MonoidalCategoryStruct.associator X Y Z).unop = (MonoidalCategoryStruct.associator (Opposite.unop X) (Opposite.unop Y) (Opposite.unop Z)).symm
                  source
                  @[simp]
                  theorem CategoryTheory.op_hom_associator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y Z : C) :
                  (MonoidalCategoryStruct.associator X Y Z).hom.op = (MonoidalCategoryStruct.associator (Opposite.op X) (Opposite.op Y) (Opposite.op Z)).inv
                  source
                  @[simp]
                  theorem CategoryTheory.unop_hom_associator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y Z : Cᵒᵖ) :
                  (MonoidalCategoryStruct.associator X Y Z).hom.unop = (MonoidalCategoryStruct.associator (Opposite.unop X) (Opposite.unop Y) (Opposite.unop Z)).inv
                  source
                  @[simp]
                  theorem CategoryTheory.op_inv_associator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y Z : C) :
                  (MonoidalCategoryStruct.associator X Y Z).inv.op = (MonoidalCategoryStruct.associator (Opposite.op X) (Opposite.op Y) (Opposite.op Z)).hom
                  source
                  @[simp]
                  theorem CategoryTheory.unop_inv_associator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y Z : Cᵒᵖ) :
                  (MonoidalCategoryStruct.associator X Y Z).inv.unop = (MonoidalCategoryStruct.associator (Opposite.unop X) (Opposite.unop Y) (Opposite.unop Z)).hom
                  source
                  @[simp]
                  theorem CategoryTheory.op_leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) :
                  (MonoidalCategoryStruct.leftUnitor X).op = (MonoidalCategoryStruct.leftUnitor (Opposite.op X)).symm
                  source
                  @[simp]
                  theorem CategoryTheory.unop_leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᵒᵖ) :
                  (MonoidalCategoryStruct.leftUnitor X).unop = (MonoidalCategoryStruct.leftUnitor (Opposite.unop X)).symm
                  source
                  @[simp]
                  theorem CategoryTheory.op_hom_leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) :
                  (MonoidalCategoryStruct.leftUnitor X).hom.op = (MonoidalCategoryStruct.leftUnitor (Opposite.op X)).inv
                  source
                  @[simp]
                  theorem CategoryTheory.unop_hom_leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᵒᵖ) :
                  (MonoidalCategoryStruct.leftUnitor X).hom.unop = (MonoidalCategoryStruct.leftUnitor (Opposite.unop X)).inv
                  source
                  @[simp]
                  theorem CategoryTheory.op_inv_leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) :
                  (MonoidalCategoryStruct.leftUnitor X).inv.op = (MonoidalCategoryStruct.leftUnitor (Opposite.op X)).hom
                  source
                  @[simp]
                  theorem CategoryTheory.unop_inv_leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᵒᵖ) :
                  (MonoidalCategoryStruct.leftUnitor X).inv.unop = (MonoidalCategoryStruct.leftUnitor (Opposite.unop X)).hom
                  source
                  @[simp]
                  theorem CategoryTheory.op_rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) :
                  (MonoidalCategoryStruct.rightUnitor X).op = (MonoidalCategoryStruct.rightUnitor (Opposite.op X)).symm
                  source
                  @[simp]
                  theorem CategoryTheory.unop_rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᵒᵖ) :
                  (MonoidalCategoryStruct.rightUnitor X).unop = (MonoidalCategoryStruct.rightUnitor (Opposite.unop X)).symm
                  source
                  @[simp]
                  theorem CategoryTheory.op_hom_rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) :
                  (MonoidalCategoryStruct.rightUnitor X).hom.op = (MonoidalCategoryStruct.rightUnitor (Opposite.op X)).inv
                  source
                  @[simp]
                  theorem CategoryTheory.unop_hom_rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᵒᵖ) :
                  (MonoidalCategoryStruct.rightUnitor X).hom.unop = (MonoidalCategoryStruct.rightUnitor (Opposite.unop X)).inv
                  source
                  @[simp]
                  theorem CategoryTheory.op_inv_rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) :
                  (MonoidalCategoryStruct.rightUnitor X).inv.op = (MonoidalCategoryStruct.rightUnitor (Opposite.op X)).hom
                  source
                  @[simp]
                  theorem CategoryTheory.unop_inv_rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᵒᵖ) :
                  (MonoidalCategoryStruct.rightUnitor X).inv.unop = (MonoidalCategoryStruct.rightUnitor (Opposite.unop X)).hom
                  source
                  theorem CategoryTheory.op_tensor_op {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) :
                  MonoidalCategoryStruct.tensorHom f.op g.op = (MonoidalCategoryStruct.tensorHom f g).op
                  source
                  theorem CategoryTheory.unop_tensor_unop {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {W X Y Z : Cᵒᵖ} (f : W ⟶ X) (g : Y ⟶ Z) :
                  MonoidalCategoryStruct.tensorHom f.unop g.unop = (MonoidalCategoryStruct.tensorHom f g).unop
                  source
                  instance CategoryTheory.monoidalCategoryMop {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :
                  MonoidalCategory Cᴹᵒᵖ
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  @[simp]
                  theorem CategoryTheory.mop_tensorObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : C) :
                  { unmop := MonoidalCategoryStruct.tensorObj X Y } = MonoidalCategoryStruct.tensorObj { unmop := Y } { unmop := X }
                  source
                  @[simp]
                  theorem CategoryTheory.unmop_tensorObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : Cᴹᵒᵖ) :
                  (MonoidalCategoryStruct.tensorObj X Y).unmop = MonoidalCategoryStruct.tensorObj Y.unmop X.unmop
                  source
                  @[simp]
                  theorem CategoryTheory.mop_tensorUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :
                  { unmop := MonoidalCategoryStruct.tensorUnit C } = MonoidalCategoryStruct.tensorUnit Cᴹᵒᵖ
                  source
                  @[simp]
                  theorem CategoryTheory.unmop_tensorUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :
                  (MonoidalCategoryStruct.tensorUnit Cᴹᵒᵖ).unmop = MonoidalCategoryStruct.tensorUnit C
                  source
                  @[simp]
                  theorem CategoryTheory.mop_tensorHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
                  (MonoidalCategoryStruct.tensorHom f g).mop = MonoidalCategoryStruct.tensorHom g.mop f.mop
                  source
                  @[simp]
                  theorem CategoryTheory.unmop_tensorHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X₁ Y₁ X₂ Y₂ : Cᴹᵒᵖ} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
                  (MonoidalCategoryStruct.tensorHom f g).unmop = MonoidalCategoryStruct.tensorHom g.unmop f.unmop
                  source
                  @[simp]
                  theorem CategoryTheory.mop_whiskerLeft {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z) :
                  (MonoidalCategoryStruct.whiskerLeft X f).mop = MonoidalCategoryStruct.whiskerRight f.mop { unmop := X }
                  source
                  @[simp]
                  theorem CategoryTheory.unmop_whiskerLeft {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᴹᵒᵖ) {Y Z : Cᴹᵒᵖ} (f : Y ⟶ Z) :
                  (MonoidalCategoryStruct.whiskerLeft X f).unmop = MonoidalCategoryStruct.whiskerRight f.unmop X.unmop
                  source
                  @[simp]
                  theorem CategoryTheory.mop_whiskerRight {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : C} (f : X ⟶ Y) (Z : C) :
                  (MonoidalCategoryStruct.whiskerRight f Z).mop = MonoidalCategoryStruct.whiskerLeft { unmop := Z } f.mop
                  source
                  @[simp]
                  theorem CategoryTheory.unmop_whiskerRight {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : Cᴹᵒᵖ} (f : X ⟶ Y) (Z : Cᴹᵒᵖ) :
                  (MonoidalCategoryStruct.whiskerRight f Z).unmop = MonoidalCategoryStruct.whiskerLeft Z.unmop f.unmop
                  source
                  @[simp]
                  theorem CategoryTheory.mop_associator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y Z : C) :
                  (MonoidalCategoryStruct.associator X Y Z).mop = (MonoidalCategoryStruct.associator { unmop := Z } { unmop := Y } { unmop := X }).symm
                  source
                  @[simp]
                  theorem CategoryTheory.unmop_associator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y Z : Cᴹᵒᵖ) :
                  (MonoidalCategoryStruct.associator X Y Z).unmop = (MonoidalCategoryStruct.associator Z.unmop Y.unmop X.unmop).symm
                  source
                  @[simp]
                  theorem CategoryTheory.mop_hom_associator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y Z : C) :
                  (MonoidalCategoryStruct.associator X Y Z).hom.mop = (MonoidalCategoryStruct.associator { unmop := Z } { unmop := Y } { unmop := X }).inv
                  source
                  @[simp]
                  theorem CategoryTheory.unmop_hom_associator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y Z : Cᴹᵒᵖ) :
                  (MonoidalCategoryStruct.associator X Y Z).hom.unmop = (MonoidalCategoryStruct.associator Z.unmop Y.unmop X.unmop).inv
                  source
                  @[simp]
                  theorem CategoryTheory.mop_inv_associator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y Z : C) :
                  (MonoidalCategoryStruct.associator X Y Z).inv.mop = (MonoidalCategoryStruct.associator { unmop := Z } { unmop := Y } { unmop := X }).hom
                  source
                  @[simp]
                  theorem CategoryTheory.unmop_inv_associator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y Z : Cᴹᵒᵖ) :
                  (MonoidalCategoryStruct.associator X Y Z).inv.unmop = (MonoidalCategoryStruct.associator Z.unmop Y.unmop X.unmop).hom
                  source
                  @[simp]
                  theorem CategoryTheory.mop_leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) :
                  (MonoidalCategoryStruct.leftUnitor X).mop = MonoidalCategoryStruct.rightUnitor { unmop := X }
                  source
                  @[simp]
                  theorem CategoryTheory.unmop_leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᴹᵒᵖ) :
                  (MonoidalCategoryStruct.leftUnitor X).unmop = MonoidalCategoryStruct.rightUnitor X.unmop
                  source
                  @[simp]
                  theorem CategoryTheory.mop_hom_leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) :
                  (MonoidalCategoryStruct.leftUnitor X).hom.mop = (MonoidalCategoryStruct.rightUnitor { unmop := X }).hom
                  source
                  @[simp]
                  theorem CategoryTheory.unmop_hom_leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᴹᵒᵖ) :
                  (MonoidalCategoryStruct.leftUnitor X).hom.unmop = (MonoidalCategoryStruct.rightUnitor X.unmop).hom
                  source
                  @[simp]
                  theorem CategoryTheory.mop_inv_leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) :
                  (MonoidalCategoryStruct.leftUnitor X).inv.mop = (MonoidalCategoryStruct.rightUnitor { unmop := X }).inv
                  source
                  @[simp]
                  theorem CategoryTheory.unmop_inv_leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᴹᵒᵖ) :
                  (MonoidalCategoryStruct.leftUnitor X).inv.unmop = (MonoidalCategoryStruct.rightUnitor X.unmop).inv
                  source
                  @[simp]
                  theorem CategoryTheory.mop_rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) :
                  (MonoidalCategoryStruct.rightUnitor X).mop = MonoidalCategoryStruct.leftUnitor { unmop := X }
                  source
                  @[simp]
                  theorem CategoryTheory.unmop_rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᴹᵒᵖ) :
                  (MonoidalCategoryStruct.rightUnitor X).unmop = MonoidalCategoryStruct.leftUnitor X.unmop
                  source
                  @[simp]
                  theorem CategoryTheory.mop_hom_rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) :
                  (MonoidalCategoryStruct.rightUnitor X).hom.mop = (MonoidalCategoryStruct.leftUnitor { unmop := X }).hom
                  source
                  @[simp]
                  theorem CategoryTheory.unmop_hom_rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᴹᵒᵖ) :
                  (MonoidalCategoryStruct.rightUnitor X).hom.unmop = (MonoidalCategoryStruct.leftUnitor X.unmop).hom
                  source
                  @[simp]
                  theorem CategoryTheory.mop_inv_rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) :
                  (MonoidalCategoryStruct.rightUnitor X).inv.mop = (MonoidalCategoryStruct.leftUnitor { unmop := X }).inv
                  source
                  @[simp]
                  theorem CategoryTheory.unmop_inv_rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᴹᵒᵖ) :
                  (MonoidalCategoryStruct.rightUnitor X).inv.unmop = (MonoidalCategoryStruct.leftUnitor X.unmop).inv
                  source
                  def CategoryTheory.MonoidalOpposite.mopEquiv (C : Type u₁) [Category.{v₁, u₁} C] :
                  C ≌ Cᴹᵒᵖ

                  The (identity) equivalence between C and its monoidal opposite.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalOpposite.mopEquiv_counitIso (C : Type u₁) [Category.{v₁, u₁} C] :
                    (mopEquiv C).counitIso = Iso.refl ((unmopFunctor C).comp (mopFunctor C))
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalOpposite.mopEquiv_inverse (C : Type u₁) [Category.{v₁, u₁} C] :
                    (mopEquiv C).inverse = unmopFunctor C
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalOpposite.mopEquiv_unitIso (C : Type u₁) [Category.{v₁, u₁} C] :
                    (mopEquiv C).unitIso = Iso.refl (Functor.id C)
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalOpposite.mopEquiv_functor (C : Type u₁) [Category.{v₁, u₁} C] :
                    (mopEquiv C).functor = mopFunctor C
                    source
                    def CategoryTheory.MonoidalOpposite.unmopEquiv (C : Type u₁) [Category.{v₁, u₁} C] :
                    Cᴹᵒᵖ ≌ C

                    The (identity) equivalence between Cᴹᵒᵖ and C.

                    Equations
                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.MonoidalOpposite.unmopEquiv_inverse_map_unmop (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
                      ((unmopEquiv C).inverse.map f).unmop = f
                      source
                      @[simp]
                      theorem CategoryTheory.MonoidalOpposite.unmopEquiv_counitIso_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (X : C) :
                      (unmopEquiv C).counitIso.inv.app X = CategoryStruct.id X
                      source
                      @[simp]
                      theorem CategoryTheory.MonoidalOpposite.unmopEquiv_unitIso_hom_app_unmop (C : Type u₁) [Category.{v₁, u₁} C] (X : Cᴹᵒᵖ) :
                      ((unmopEquiv C).unitIso.hom.app X).unmop = CategoryStruct.id X.unmop
                      source
                      @[simp]
                      theorem CategoryTheory.MonoidalOpposite.unmopEquiv_functor_map (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : Cᴹᵒᵖ} (f : X✝ ⟶ Y✝) :
                      (unmopEquiv C).functor.map f = f.unmop
                      source
                      @[simp]
                      theorem CategoryTheory.MonoidalOpposite.unmopEquiv_unitIso_inv_app_unmop (C : Type u₁) [Category.{v₁, u₁} C] (X : Cᴹᵒᵖ) :
                      ((unmopEquiv C).unitIso.inv.app X).unmop = CategoryStruct.id X.unmop
                      source
                      @[simp]
                      theorem CategoryTheory.MonoidalOpposite.unmopEquiv_inverse_obj_unmop (C : Type u₁) [Category.{v₁, u₁} C] (unmop : C) :
                      ((unmopEquiv C).inverse.obj unmop).unmop = unmop
                      source
                      @[simp]
                      theorem CategoryTheory.MonoidalOpposite.unmopEquiv_counitIso_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (X : C) :
                      (unmopEquiv C).counitIso.hom.app X = CategoryStruct.id X
                      source
                      @[simp]
                      theorem CategoryTheory.MonoidalOpposite.unmopEquiv_functor_obj (C : Type u₁) [Category.{v₁, u₁} C] (self : Cᴹᵒᵖ) :
                      (unmopEquiv C).functor.obj self = self.unmop
                      source
                      def CategoryTheory.MonoidalOpposite.mopMopEquivalence (C : Type u₁) [Category.{v₁, u₁} C] :
                      Cᴹᵒᵖᴹᵒᵖ ≌ C

                      The equivalence between C and its monoidal opposite's monoidal opposite.

                      Equations
                      Instances For
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_functor_obj (C : Type u₁) [Category.{v₁, u₁} C] (X : Cᴹᵒᵖᴹᵒᵖ) :
                        (mopMopEquivalence C).functor.obj X = X.unmop.unmop
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_counitIso_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (X : C) :
                        (mopMopEquivalence C).counitIso.hom.app X = CategoryStruct.id X
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_functor_map (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : Cᴹᵒᵖᴹᵒᵖ} (f : X✝ ⟶ Y✝) :
                        (mopMopEquivalence C).functor.map f = f.unmop.unmop
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_counitIso_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (X : C) :
                        (mopMopEquivalence C).counitIso.inv.app X = CategoryStruct.id X
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_unitIso_inv_app_unmop_unmop (C : Type u₁) [Category.{v₁, u₁} C] (X : Cᴹᵒᵖᴹᵒᵖ) :
                        ((mopMopEquivalence C).unitIso.inv.app X).unmop.unmop = (CategoryStruct.id X.unmop).unmop
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_inverse_map_unmop_unmop (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
                        ((mopMopEquivalence C).inverse.map f).unmop.unmop = f
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_inverse_obj_unmop_unmop (C : Type u₁) [Category.{v₁, u₁} C] (X : C) :
                        ((mopMopEquivalence C).inverse.obj X).unmop.unmop = X
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_unitIso_hom_app_unmop_unmop (C : Type u₁) [Category.{v₁, u₁} C] (X : Cᴹᵒᵖᴹᵒᵖ) :
                        ((mopMopEquivalence C).unitIso.hom.app X).unmop.unmop = (CategoryStruct.id X.unmop).unmop
                        source
                        instance CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] :
                        (mopMopEquivalence C).functor.Monoidal
                        Equations
                        • One or more equations did not get rendered due to their size.
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_δ (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : Cᴹᵒᵖᴹᵒᵖ) :
                        Functor.OplaxMonoidal.δ (mopMopEquivalence C).functor X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X.unmop.unmop Y.unmop.unmop)
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_ε (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] :
                        Functor.LaxMonoidal.ε (mopMopEquivalence C).functor = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_μ (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : Cᴹᵒᵖᴹᵒᵖ) :
                        Functor.LaxMonoidal.μ (mopMopEquivalence C).functor X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X.unmop.unmop Y.unmop.unmop)
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_η (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] :
                        Functor.OplaxMonoidal.η (mopMopEquivalence C).functor = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)
                        source
                        instance CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] :
                        (mopMopEquivalence C).inverse.Monoidal
                        Equations
                        • One or more equations did not get rendered due to their size.
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal_ε_unmop_unmop (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] :
                        (Functor.LaxMonoidal.ε (mopMopEquivalence C).inverse).unmop.unmop = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal_δ_unmop_unmop (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : C) :
                        (Functor.OplaxMonoidal.δ (mopMopEquivalence C).inverse X Y).unmop.unmop = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X Y)
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal_η_unmop_unmop (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] :
                        (Functor.OplaxMonoidal.η (mopMopEquivalence C).inverse).unmop.unmop = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal_μ_unmop_unmop (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : C) :
                        (Functor.LaxMonoidal.μ (mopMopEquivalence C).inverse X Y).unmop.unmop = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X Y)
                        source
                        instance CategoryTheory.instIsMonoidalMonoidalOppositeMopMopEquivalence (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] :
                        (MonoidalOpposite.mopMopEquivalence C).IsMonoidal
                        source
                        def CategoryTheory.MonoidalOpposite.tensorIso (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] :
                        MonoidalCategory.tensor Cᴹᵒᵖ ≅ ((unmopFunctor C).prod (unmopFunctor C)).comp ((Prod.swap C C).comp ((MonoidalCategory.tensor C).comp (mopFunctor C)))

                        The identification mop X ⊗ mop Y = mop (Y ⊗ X) as a natural isomorphism.

                        Equations
                        Instances For
                          source
                          @[simp]
                          theorem CategoryTheory.MonoidalOpposite.tensorIso_inv_app_unmop (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᴹᵒᵖ × Cᴹᵒᵖ) :
                          ((tensorIso C).inv.app X).unmop = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X.2.unmop X.1.unmop)
                          source
                          @[simp]
                          theorem CategoryTheory.MonoidalOpposite.tensorIso_hom_app_unmop (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᴹᵒᵖ × Cᴹᵒᵖ) :
                          ((tensorIso C).hom.app X).unmop = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X.2.unmop X.1.unmop)
                          source
                          def CategoryTheory.MonoidalOpposite.tensorLeftIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᴹᵒᵖ) :
                          MonoidalCategory.tensorLeft X ≅ (unmopFunctor C).comp ((MonoidalCategory.tensorRight X.unmop).comp (mopFunctor C))

                          The identification X ⊗ - = mop (- ⊗ unmop X) as a natural isomorphism.

                          Equations
                          Instances For
                            source
                            @[simp]
                            theorem CategoryTheory.MonoidalOpposite.tensorLeftIso_inv_app_unmop {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X X✝ : Cᴹᵒᵖ) :
                            (X.tensorLeftIso.inv.app X✝).unmop = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X✝.unmop X.unmop)
                            source
                            @[simp]
                            theorem CategoryTheory.MonoidalOpposite.tensorLeftIso_hom_app_unmop {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X X✝ : Cᴹᵒᵖ) :
                            (X.tensorLeftIso.hom.app X✝).unmop = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X✝.unmop X.unmop)
                            source
                            def CategoryTheory.MonoidalOpposite.tensorLeftMopIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) :
                            MonoidalCategory.tensorLeft { unmop := X } ≅ (unmopFunctor C).comp ((MonoidalCategory.tensorRight X).comp (mopFunctor C))

                            The identification mop X ⊗ - = mop (- ⊗ X) as a natural isomorphism.

                            Equations
                            Instances For
                              source
                              @[simp]
                              theorem CategoryTheory.MonoidalOpposite.tensorLeftMopIso_inv_app_unmop {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) (X✝ : Cᴹᵒᵖ) :
                              ((tensorLeftMopIso X).inv.app X✝).unmop = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X✝.unmop X)
                              source
                              @[simp]
                              theorem CategoryTheory.MonoidalOpposite.tensorLeftMopIso_hom_app_unmop {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) (X✝ : Cᴹᵒᵖ) :
                              ((tensorLeftMopIso X).hom.app X✝).unmop = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X✝.unmop X)
                              source
                              def CategoryTheory.MonoidalOpposite.tensorLeftUnmopIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᴹᵒᵖ) :
                              MonoidalCategory.tensorLeft X.unmop ≅ (mopFunctor C).comp ((MonoidalCategory.tensorRight X).comp (unmopFunctor C))

                              The identification unmop X ⊗ - = unmop (mop - ⊗ X) as a natural isomorphism.

                              Equations
                              Instances For
                                source
                                @[simp]
                                theorem CategoryTheory.MonoidalOpposite.tensorLeftUnmopIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᴹᵒᵖ) (X✝ : C) :
                                X.tensorLeftUnmopIso.hom.app X✝ = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X.unmop X✝)
                                source
                                @[simp]
                                theorem CategoryTheory.MonoidalOpposite.tensorLeftUnmopIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᴹᵒᵖ) (X✝ : C) :
                                X.tensorLeftUnmopIso.inv.app X✝ = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X.unmop X✝)
                                source
                                def CategoryTheory.MonoidalOpposite.tensorRightIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᴹᵒᵖ) :
                                MonoidalCategory.tensorRight X ≅ (unmopFunctor C).comp ((MonoidalCategory.tensorLeft X.unmop).comp (mopFunctor C))

                                The identification - ⊗ X = mop (unmop X ⊗ -) as a natural isomorphism.

                                Equations
                                Instances For
                                  source
                                  @[simp]
                                  theorem CategoryTheory.MonoidalOpposite.tensorRightIso_hom_app_unmop {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X X✝ : Cᴹᵒᵖ) :
                                  (X.tensorRightIso.hom.app X✝).unmop = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X.unmop X✝.unmop)
                                  source
                                  @[simp]
                                  theorem CategoryTheory.MonoidalOpposite.tensorRightIso_inv_app_unmop {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X X✝ : Cᴹᵒᵖ) :
                                  (X.tensorRightIso.inv.app X✝).unmop = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X.unmop X✝.unmop)
                                  source
                                  def CategoryTheory.MonoidalOpposite.tensorRightMopIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) :
                                  MonoidalCategory.tensorRight { unmop := X } ≅ (unmopFunctor C).comp ((MonoidalCategory.tensorLeft X).comp (mopFunctor C))

                                  The identification - ⊗ mop X = mop (- ⊗ unmop X) as a natural isomorphism.

                                  Equations
                                  Instances For
                                    source
                                    @[simp]
                                    theorem CategoryTheory.MonoidalOpposite.tensorRightMopIso_inv_app_unmop {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) (X✝ : Cᴹᵒᵖ) :
                                    ((tensorRightMopIso X).inv.app X✝).unmop = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X X✝.unmop)
                                    source
                                    @[simp]
                                    theorem CategoryTheory.MonoidalOpposite.tensorRightMopIso_hom_app_unmop {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) (X✝ : Cᴹᵒᵖ) :
                                    ((tensorRightMopIso X).hom.app X✝).unmop = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X X✝.unmop)
                                    source
                                    def CategoryTheory.MonoidalOpposite.tensorRightUnmopIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᴹᵒᵖ) :
                                    MonoidalCategory.tensorRight X.unmop ≅ (mopFunctor C).comp ((MonoidalCategory.tensorLeft X).comp (unmopFunctor C))

                                    The identification - ⊗ unmop X = unmop (X ⊗ mop -) as a natural isomorphism.

                                    Equations
                                    Instances For
                                      source
                                      @[simp]
                                      theorem CategoryTheory.MonoidalOpposite.tensorRightUnmopIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᴹᵒᵖ) (X✝ : C) :
                                      X.tensorRightUnmopIso.inv.app X✝ = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X✝ X.unmop)
                                      source
                                      @[simp]
                                      theorem CategoryTheory.MonoidalOpposite.tensorRightUnmopIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Cᴹᵒᵖ) (X✝ : C) :
                                      X.tensorRightUnmopIso.hom.app X✝ = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X✝ X.unmop)
                                      source
                                      instance CategoryTheory.monoidalOpOp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :
                                      (opOp C).Monoidal
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      source
                                      @[simp]
                                      theorem CategoryTheory.monoidalOpOp_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :
                                      Functor.LaxMonoidal.ε (opOp C) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit Cᵒᵖᵒᵖ)
                                      source
                                      @[simp]
                                      theorem CategoryTheory.monoidalOpOp_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : C) :
                                      Functor.LaxMonoidal.μ (opOp C) X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj ((opOp C).obj X) ((opOp C).obj Y))
                                      source
                                      @[simp]
                                      theorem CategoryTheory.monoidalOpOp_δ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : C) :
                                      Functor.OplaxMonoidal.δ (opOp C) X Y = CategoryStruct.id ((opOp C).obj (MonoidalCategoryStruct.tensorObj X Y))
                                      source
                                      @[simp]
                                      theorem CategoryTheory.monoidalOpOp_η {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :
                                      Functor.OplaxMonoidal.η (opOp C) = CategoryStruct.id ((opOp C).obj (MonoidalCategoryStruct.tensorUnit C))
                                      source
                                      instance CategoryTheory.monoidalUnopUnop {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :
                                      (unopUnop C).Monoidal
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      source
                                      @[simp]
                                      theorem CategoryTheory.monoidalUnopUnop_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : Cᵒᵖᵒᵖ) :
                                      Functor.LaxMonoidal.μ (unopUnop C) X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj ((unopUnop C).obj X) ((unopUnop C).obj Y))
                                      source
                                      @[simp]
                                      theorem CategoryTheory.monoidalUnopUnop_η {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :
                                      Functor.OplaxMonoidal.η (unopUnop C) = CategoryStruct.id ((unopUnop C).obj (MonoidalCategoryStruct.tensorUnit Cᵒᵖᵒᵖ))
                                      source
                                      @[simp]
                                      theorem CategoryTheory.monoidalUnopUnop_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :
                                      Functor.LaxMonoidal.ε (unopUnop C) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)
                                      source
                                      @[simp]
                                      theorem CategoryTheory.monoidalUnopUnop_δ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : Cᵒᵖᵒᵖ) :
                                      Functor.OplaxMonoidal.δ (unopUnop C) X Y = CategoryStruct.id ((unopUnop C).obj (MonoidalCategoryStruct.tensorObj X Y))
                                      source
                                      instance CategoryTheory.instMonoidalOppositeFunctorOpOpEquivalence {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :
                                      (opOpEquivalence C).functor.Monoidal
                                      Equations
                                      source
                                      instance CategoryTheory.instMonoidalOppositeInverseOpOpEquivalence {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :
                                      (opOpEquivalence C).inverse.Monoidal
                                      Equations
                                      source
                                      @[deprecated CategoryTheory.monoidalOpOp_ε (since := "2025-06-08")]
                                      theorem CategoryTheory.opOp_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :
                                      Functor.LaxMonoidal.ε (opOp C) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit Cᵒᵖᵒᵖ)

                                      Alias of CategoryTheory.monoidalOpOp_ε.

                                      source
                                      @[deprecated CategoryTheory.monoidalOpOp_η (since := "2025-06-08")]
                                      theorem CategoryTheory.opOp_η {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :
                                      Functor.OplaxMonoidal.η (opOp C) = CategoryStruct.id ((opOp C).obj (MonoidalCategoryStruct.tensorUnit C))

                                      Alias of CategoryTheory.monoidalOpOp_η.

                                      source
                                      @[deprecated CategoryTheory.monoidalUnopUnop_ε (since := "2025-06-08")]
                                      theorem CategoryTheory.unopUnop_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :
                                      Functor.LaxMonoidal.ε (unopUnop C) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

                                      Alias of CategoryTheory.monoidalUnopUnop_ε.

                                      source
                                      @[deprecated CategoryTheory.monoidalUnopUnop_η (since := "2025-06-08")]
                                      theorem CategoryTheory.unopUnop_η {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :
                                      Functor.OplaxMonoidal.η (unopUnop C) = CategoryStruct.id ((unopUnop C).obj (MonoidalCategoryStruct.tensorUnit Cᵒᵖᵒᵖ))

                                      Alias of CategoryTheory.monoidalUnopUnop_η.

                                      source
                                      @[deprecated CategoryTheory.monoidalOpOp_μ (since := "2025-06-08")]
                                      theorem CategoryTheory.opOp_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : C) :
                                      Functor.LaxMonoidal.μ (opOp C) X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj ((opOp C).obj X) ((opOp C).obj Y))

                                      Alias of CategoryTheory.monoidalOpOp_μ.

                                      source
                                      @[deprecated CategoryTheory.monoidalOpOp_δ (since := "2025-06-08")]
                                      theorem CategoryTheory.opOp_δ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : C) :
                                      Functor.OplaxMonoidal.δ (opOp C) X Y = CategoryStruct.id ((opOp C).obj (MonoidalCategoryStruct.tensorObj X Y))

                                      Alias of CategoryTheory.monoidalOpOp_δ.

                                      source
                                      @[deprecated CategoryTheory.monoidalUnopUnop_μ (since := "2025-06-08")]
                                      theorem CategoryTheory.unopUnop_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : Cᵒᵖᵒᵖ) :
                                      Functor.LaxMonoidal.μ (unopUnop C) X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj ((unopUnop C).obj X) ((unopUnop C).obj Y))

                                      Alias of CategoryTheory.monoidalUnopUnop_μ.

                                      source
                                      @[deprecated CategoryTheory.monoidalUnopUnop_δ (since := "2025-06-08")]
                                      theorem CategoryTheory.unopUnop_δ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : Cᵒᵖᵒᵖ) :
                                      Functor.OplaxMonoidal.δ (unopUnop C) X Y = CategoryStruct.id ((unopUnop C).obj (MonoidalCategoryStruct.tensorObj X Y))

                                      Alias of CategoryTheory.monoidalUnopUnop_δ.

                                      source
                                      instance CategoryTheory.instIsMonoidalOppositeOpOpEquivalence {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :
                                      (opOpEquivalence C).IsMonoidal