Monoidal opposites

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

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

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

• mop :: (
• unmop : C

  The object of C represented by x : MonoidalOpposite C.

• )

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

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

Equations

• CategoryTheory.MonoidalOpposite.«term_ᴹᵒᵖ» = Lean.ParserDescr.trailingNode `CategoryTheory.MonoidalOpposite.term_ᴹᵒᵖ 1024 0 (Lean.ParserDescr.symbol "ᴹᵒᵖ")

theorem CategoryTheory.MonoidalOpposite.mop_injective {C : Type u₁} : Function.Injective CategoryTheory.MonoidalOpposite.mop

theorem CategoryTheory.MonoidalOpposite.unmop_injective {C : Type u₁} : Function.Injective CategoryTheory.MonoidalOpposite.unmop

theorem CategoryTheory.MonoidalOpposite.mop_inj_iff {C : Type u₁} (x : C) (y : C) : { unmop := x } = { unmop := y } ↔ x = y

@[simp]

theorem CategoryTheory.MonoidalOpposite.unmop_inj_iff {C : Type u₁} (x : Cᴹᵒᵖ) (y : Cᴹᵒᵖ) : x.unmop = y.unmop ↔ x = y

@[simp]

theorem CategoryTheory.MonoidalOpposite.mop_unmop {C : Type u₁} (X : Cᴹᵒᵖ) : { unmop := X.unmop } = X

theorem CategoryTheory.MonoidalOpposite.unmop_mop {C : Type u₁} (X : C) : { unmop := X }.unmop = X

instance CategoryTheory.MonoidalOpposite.monoidalOppositeCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Category.{v₁, u₁} Cᴹᵒᵖ

Equations

• CategoryTheory.MonoidalOpposite.monoidalOppositeCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯

def Quiver.Hom.mop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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

• Quiver.Hom.mop f = { unmop := f }

def Quiver.Hom.unmop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᴹᵒᵖ} {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

• Quiver.Hom.unmop f = f.unmop

theorem Quiver.Hom.mop_inj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} : Function.Injective Quiver.Hom.mop

theorem Quiver.Hom.unmop_inj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᴹᵒᵖ} {Y : Cᴹᵒᵖ} : Function.Injective Quiver.Hom.unmop

@[simp]

theorem Quiver.Hom.unmop_mop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {f : X ⟶ Y} : Quiver.Hom.unmop (Quiver.Hom.mop f) = f

@[simp]

theorem Quiver.Hom.mop_unmop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᴹᵒᵖ} {Y : Cᴹᵒᵖ} {f : X ⟶ Y} : Quiver.Hom.mop (Quiver.Hom.unmop f) = f

@[simp]

theorem CategoryTheory.mop_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} : Quiver.Hom.mop (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (Quiver.Hom.mop f) (Quiver.Hom.mop g)

@[simp]

theorem CategoryTheory.mop_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : Quiver.Hom.mop (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id { unmop := X }

@[simp]

theorem CategoryTheory.unmop_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᴹᵒᵖ} {Y : Cᴹᵒᵖ} {Z : Cᴹᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} : Quiver.Hom.unmop (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (Quiver.Hom.unmop f) (Quiver.Hom.unmop g)

@[simp]

theorem CategoryTheory.unmop_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᴹᵒᵖ} : Quiver.Hom.unmop (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id X.unmop

@[simp]

theorem CategoryTheory.unmop_id_mop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : Quiver.Hom.unmop (CategoryTheory.CategoryStruct.id { unmop := X }) = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.mop_id_unmop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᴹᵒᵖ} : Quiver.Hom.mop (CategoryTheory.CategoryStruct.id X.unmop) = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.mopFunctor_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : ∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.mopFunctor C).map f = Quiver.Hom.mop f

@[simp]

theorem CategoryTheory.mopFunctor_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (unmop : C) : (CategoryTheory.mopFunctor C).obj unmop = { unmop := unmop }

def CategoryTheory.mopFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Functor C Cᴹᵒᵖ

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

Equations

• CategoryTheory.mopFunctor C = { toPrefunctor := { obj := CategoryTheory.MonoidalOpposite.mop, map := fun {X Y : C} => Quiver.Hom.mop }, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.unmopFunctor_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (self : Cᴹᵒᵖ) : (CategoryTheory.unmopFunctor C).obj self = self.unmop

@[simp]

theorem CategoryTheory.unmopFunctor_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : ∀ {X Y : Cᴹᵒᵖ} (f : X ⟶ Y), (CategoryTheory.unmopFunctor C).map f = Quiver.Hom.unmop f

def CategoryTheory.unmopFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Functor Cᴹᵒᵖ C

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

Equations

• CategoryTheory.unmopFunctor C = { toPrefunctor := { obj := CategoryTheory.MonoidalOpposite.unmop, map := fun {X Y : Cᴹᵒᵖ} => Quiver.Hom.unmop }, map_id := ⋯, map_comp := ⋯ }

@[reducible]

def CategoryTheory.Iso.mop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ≅ Y) : { unmop := X } ≅ { unmop := Y }

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

Equations

• CategoryTheory.Iso.mop f = (CategoryTheory.mopFunctor C).mapIso f

@[reducible]

def CategoryTheory.Iso.unmop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᴹᵒᵖ} {Y : Cᴹᵒᵖ} (f : X ≅ Y) : X.unmop ≅ Y.unmop

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

Equations

• CategoryTheory.Iso.unmop f = (CategoryTheory.unmopFunctor C).mapIso f

instance CategoryTheory.IsIso.instIsIsoMonoidalOppositeMonoidalOppositeCategoryMopMop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso (Quiver.Hom.mop f)

Equations

• ⋯ = ⋯

instance CategoryTheory.IsIso.instIsIsoUnmopUnmop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᴹᵒᵖ} {Y : Cᴹᵒᵖ} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso (Quiver.Hom.unmop f)

Equations

• ⋯ = ⋯

instance CategoryTheory.monoidalCategoryOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.MonoidalCategory Cᵒᵖ

Equations

• CategoryTheory.monoidalCategoryOp = CategoryTheory.MonoidalCategory.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.op_tensorObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) : Opposite.op (CategoryTheory.MonoidalCategory.tensorObj X Y) = CategoryTheory.MonoidalCategory.tensorObj (Opposite.op X) (Opposite.op Y)

@[simp]

theorem CategoryTheory.unop_tensorObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᵒᵖ) (Y : Cᵒᵖ) : (CategoryTheory.MonoidalCategory.tensorObj X Y).unop = CategoryTheory.MonoidalCategory.tensorObj X.unop Y.unop

@[simp]

theorem CategoryTheory.op_tensorUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : Opposite.op (𝟙_ C) = 𝟙_ Cᵒᵖ

@[simp]

theorem CategoryTheory.unop_tensorUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (𝟙_ Cᵒᵖ).unop = 𝟙_ C

@[simp]

theorem CategoryTheory.op_tensorHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : (CategoryTheory.MonoidalCategory.tensorHom f g).op = CategoryTheory.MonoidalCategory.tensorHom f.op g.op

@[simp]

theorem CategoryTheory.unop_tensorHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X₁ : Cᵒᵖ} {Y₁ : Cᵒᵖ} {X₂ : Cᵒᵖ} {Y₂ : Cᵒᵖ} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : (CategoryTheory.MonoidalCategory.tensorHom f g).unop = CategoryTheory.MonoidalCategory.tensorHom f.unop g.unop

@[simp]

theorem CategoryTheory.op_whiskerLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) {Y : C} {Z : C} (f : Y ⟶ Z) : (CategoryTheory.MonoidalCategory.whiskerLeft X f).op = CategoryTheory.MonoidalCategory.whiskerLeft (Opposite.op X) f.op

@[simp]

theorem CategoryTheory.unop_whiskerLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᵒᵖ) {Y : Cᵒᵖ} {Z : Cᵒᵖ} (f : Y ⟶ Z) : (CategoryTheory.MonoidalCategory.whiskerLeft X f).unop = CategoryTheory.MonoidalCategory.whiskerLeft X.unop f.unop

@[simp]

theorem CategoryTheory.op_whiskerRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} (f : X ⟶ Y) (Z : C) : (CategoryTheory.MonoidalCategory.whiskerRight f Z).op = CategoryTheory.MonoidalCategory.whiskerRight f.op (Opposite.op Z)

@[simp]

theorem CategoryTheory.unop_whiskerRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ⟶ Y) (Z : Cᵒᵖ) : (CategoryTheory.MonoidalCategory.whiskerRight f Z).unop = CategoryTheory.MonoidalCategory.whiskerRight f.unop Z.unop

@[simp]

theorem CategoryTheory.op_associator {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) : CategoryTheory.Iso.op (CategoryTheory.MonoidalCategory.associator X Y Z) = (CategoryTheory.MonoidalCategory.associator (Opposite.op X) (Opposite.op Y) (Opposite.op Z)).symm

@[simp]

theorem CategoryTheory.unop_associator {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᵒᵖ) (Y : Cᵒᵖ) (Z : Cᵒᵖ) : CategoryTheory.Iso.unop (CategoryTheory.MonoidalCategory.associator X Y Z) = (CategoryTheory.MonoidalCategory.associator X.unop Y.unop Z.unop).symm

@[simp]

theorem CategoryTheory.op_hom_associator {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) : (CategoryTheory.MonoidalCategory.associator X Y Z).hom.op = (CategoryTheory.MonoidalCategory.associator (Opposite.op X) (Opposite.op Y) (Opposite.op Z)).inv

@[simp]

theorem CategoryTheory.unop_hom_associator {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᵒᵖ) (Y : Cᵒᵖ) (Z : Cᵒᵖ) : (CategoryTheory.MonoidalCategory.associator X Y Z).hom.unop = (CategoryTheory.MonoidalCategory.associator X.unop Y.unop Z.unop).inv

@[simp]

theorem CategoryTheory.op_inv_associator {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) : (CategoryTheory.MonoidalCategory.associator X Y Z).inv.op = (CategoryTheory.MonoidalCategory.associator (Opposite.op X) (Opposite.op Y) (Opposite.op Z)).hom

@[simp]

theorem CategoryTheory.unop_inv_associator {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᵒᵖ) (Y : Cᵒᵖ) (Z : Cᵒᵖ) : (CategoryTheory.MonoidalCategory.associator X Y Z).inv.unop = (CategoryTheory.MonoidalCategory.associator X.unop Y.unop Z.unop).hom

@[simp]

theorem CategoryTheory.op_leftUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : CategoryTheory.Iso.op (CategoryTheory.MonoidalCategory.leftUnitor X) = (CategoryTheory.MonoidalCategory.leftUnitor (Opposite.op X)).symm

@[simp]

theorem CategoryTheory.unop_leftUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᵒᵖ) : CategoryTheory.Iso.unop (CategoryTheory.MonoidalCategory.leftUnitor X) = (CategoryTheory.MonoidalCategory.leftUnitor X.unop).symm

@[simp]

theorem CategoryTheory.op_hom_leftUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : (CategoryTheory.MonoidalCategory.leftUnitor X).hom.op = (CategoryTheory.MonoidalCategory.leftUnitor (Opposite.op X)).inv

@[simp]

theorem CategoryTheory.unop_hom_leftUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᵒᵖ) : (CategoryTheory.MonoidalCategory.leftUnitor X).hom.unop = (CategoryTheory.MonoidalCategory.leftUnitor X.unop).inv

@[simp]

theorem CategoryTheory.op_inv_leftUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : (CategoryTheory.MonoidalCategory.leftUnitor X).inv.op = (CategoryTheory.MonoidalCategory.leftUnitor (Opposite.op X)).hom

@[simp]

theorem CategoryTheory.unop_inv_leftUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᵒᵖ) : (CategoryTheory.MonoidalCategory.leftUnitor X).inv.unop = (CategoryTheory.MonoidalCategory.leftUnitor X.unop).hom

@[simp]

theorem CategoryTheory.op_rightUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : CategoryTheory.Iso.op (CategoryTheory.MonoidalCategory.rightUnitor X) = (CategoryTheory.MonoidalCategory.rightUnitor (Opposite.op X)).symm

@[simp]

theorem CategoryTheory.unop_rightUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᵒᵖ) : CategoryTheory.Iso.unop (CategoryTheory.MonoidalCategory.rightUnitor X) = (CategoryTheory.MonoidalCategory.rightUnitor X.unop).symm

@[simp]

theorem CategoryTheory.op_hom_rightUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : (CategoryTheory.MonoidalCategory.rightUnitor X).hom.op = (CategoryTheory.MonoidalCategory.rightUnitor (Opposite.op X)).inv

@[simp]

theorem CategoryTheory.unop_hom_rightUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᵒᵖ) : (CategoryTheory.MonoidalCategory.rightUnitor X).hom.unop = (CategoryTheory.MonoidalCategory.rightUnitor X.unop).inv

@[simp]

theorem CategoryTheory.op_inv_rightUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : (CategoryTheory.MonoidalCategory.rightUnitor X).inv.op = (CategoryTheory.MonoidalCategory.rightUnitor (Opposite.op X)).hom

@[simp]

theorem CategoryTheory.unop_inv_rightUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᵒᵖ) : (CategoryTheory.MonoidalCategory.rightUnitor X).inv.unop = (CategoryTheory.MonoidalCategory.rightUnitor X.unop).hom

instance CategoryTheory.monoidalCategoryMop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.MonoidalCategory Cᴹᵒᵖ

Equations

• CategoryTheory.monoidalCategoryMop = CategoryTheory.MonoidalCategory.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.mop_tensorObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) : { unmop := CategoryTheory.MonoidalCategory.tensorObj X Y } = CategoryTheory.MonoidalCategory.tensorObj { unmop := Y } { unmop := X }

@[simp]

theorem CategoryTheory.unmop_tensorObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) (Y : Cᴹᵒᵖ) : (CategoryTheory.MonoidalCategory.tensorObj X Y).unmop = CategoryTheory.MonoidalCategory.tensorObj Y.unmop X.unmop

@[simp]

theorem CategoryTheory.mop_tensorUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : { unmop := 𝟙_ C } = 𝟙_ Cᴹᵒᵖ

@[simp]

theorem CategoryTheory.unmop_tensorUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (𝟙_ Cᴹᵒᵖ).unmop = 𝟙_ C

@[simp]

theorem CategoryTheory.mop_tensorHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : Quiver.Hom.mop (CategoryTheory.MonoidalCategory.tensorHom f g) = CategoryTheory.MonoidalCategory.tensorHom (Quiver.Hom.mop g) (Quiver.Hom.mop f)

@[simp]

theorem CategoryTheory.unmop_tensorHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X₁ : Cᴹᵒᵖ} {Y₁ : Cᴹᵒᵖ} {X₂ : Cᴹᵒᵖ} {Y₂ : Cᴹᵒᵖ} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : Quiver.Hom.unmop (CategoryTheory.MonoidalCategory.tensorHom f g) = CategoryTheory.MonoidalCategory.tensorHom (Quiver.Hom.unmop g) (Quiver.Hom.unmop f)

@[simp]

theorem CategoryTheory.mop_whiskerLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) {Y : C} {Z : C} (f : Y ⟶ Z) : Quiver.Hom.mop (CategoryTheory.MonoidalCategory.whiskerLeft X f) = CategoryTheory.MonoidalCategory.whiskerRight (Quiver.Hom.mop f) { unmop := X }

@[simp]

theorem CategoryTheory.unmop_whiskerLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) {Y : Cᴹᵒᵖ} {Z : Cᴹᵒᵖ} (f : Y ⟶ Z) : Quiver.Hom.unmop (CategoryTheory.MonoidalCategory.whiskerLeft X f) = CategoryTheory.MonoidalCategory.whiskerRight (Quiver.Hom.unmop f) X.unmop

@[simp]

theorem CategoryTheory.mop_whiskerRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} (f : X ⟶ Y) (Z : C) : Quiver.Hom.mop (CategoryTheory.MonoidalCategory.whiskerRight f Z) = CategoryTheory.MonoidalCategory.whiskerLeft { unmop := Z } (Quiver.Hom.mop f)

@[simp]

theorem CategoryTheory.unmop_whiskerRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : Cᴹᵒᵖ} {Y : Cᴹᵒᵖ} (f : X ⟶ Y) (Z : Cᴹᵒᵖ) : Quiver.Hom.unmop (CategoryTheory.MonoidalCategory.whiskerRight f Z) = CategoryTheory.MonoidalCategory.whiskerLeft Z.unmop (Quiver.Hom.unmop f)

@[simp]

theorem CategoryTheory.mop_associator {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) : CategoryTheory.Iso.mop (CategoryTheory.MonoidalCategory.associator X Y Z) = (CategoryTheory.MonoidalCategory.associator { unmop := Z } { unmop := Y } { unmop := X }).symm

@[simp]

theorem CategoryTheory.unmop_associator {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) (Y : Cᴹᵒᵖ) (Z : Cᴹᵒᵖ) : CategoryTheory.Iso.unmop (CategoryTheory.MonoidalCategory.associator X Y Z) = (CategoryTheory.MonoidalCategory.associator Z.unmop Y.unmop X.unmop).symm

@[simp]

theorem CategoryTheory.mop_hom_associator {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) : Quiver.Hom.mop (CategoryTheory.MonoidalCategory.associator X Y Z).hom = (CategoryTheory.MonoidalCategory.associator { unmop := Z } { unmop := Y } { unmop := X }).inv

@[simp]

theorem CategoryTheory.unmop_hom_associator {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) (Y : Cᴹᵒᵖ) (Z : Cᴹᵒᵖ) : Quiver.Hom.unmop (CategoryTheory.MonoidalCategory.associator X Y Z).hom = (CategoryTheory.MonoidalCategory.associator Z.unmop Y.unmop X.unmop).inv

@[simp]

theorem CategoryTheory.mop_inv_associator {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) : Quiver.Hom.mop (CategoryTheory.MonoidalCategory.associator X Y Z).inv = (CategoryTheory.MonoidalCategory.associator { unmop := Z } { unmop := Y } { unmop := X }).hom

@[simp]

theorem CategoryTheory.unmop_inv_associator {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) (Y : Cᴹᵒᵖ) (Z : Cᴹᵒᵖ) : Quiver.Hom.unmop (CategoryTheory.MonoidalCategory.associator X Y Z).inv = (CategoryTheory.MonoidalCategory.associator Z.unmop Y.unmop X.unmop).hom

@[simp]

theorem CategoryTheory.mop_leftUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : CategoryTheory.Iso.mop (CategoryTheory.MonoidalCategory.leftUnitor X) = CategoryTheory.MonoidalCategory.rightUnitor { unmop := X }

@[simp]

theorem CategoryTheory.unmop_leftUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) : CategoryTheory.Iso.unmop (CategoryTheory.MonoidalCategory.leftUnitor X) = CategoryTheory.MonoidalCategory.rightUnitor X.unmop

@[simp]

theorem CategoryTheory.mop_hom_leftUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : Quiver.Hom.mop (CategoryTheory.MonoidalCategory.leftUnitor X).hom = (CategoryTheory.MonoidalCategory.rightUnitor { unmop := X }).hom

@[simp]

theorem CategoryTheory.unmop_hom_leftUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) : Quiver.Hom.unmop (CategoryTheory.MonoidalCategory.leftUnitor X).hom = (CategoryTheory.MonoidalCategory.rightUnitor X.unmop).hom

@[simp]

theorem CategoryTheory.mop_inv_leftUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : Quiver.Hom.mop (CategoryTheory.MonoidalCategory.leftUnitor X).inv = (CategoryTheory.MonoidalCategory.rightUnitor { unmop := X }).inv

@[simp]

theorem CategoryTheory.unmop_inv_leftUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) : Quiver.Hom.unmop (CategoryTheory.MonoidalCategory.leftUnitor X).inv = (CategoryTheory.MonoidalCategory.rightUnitor X.unmop).inv

@[simp]

theorem CategoryTheory.mop_rightUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : CategoryTheory.Iso.mop (CategoryTheory.MonoidalCategory.rightUnitor X) = CategoryTheory.MonoidalCategory.leftUnitor { unmop := X }

@[simp]

theorem CategoryTheory.unmop_rightUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) : CategoryTheory.Iso.unmop (CategoryTheory.MonoidalCategory.rightUnitor X) = CategoryTheory.MonoidalCategory.leftUnitor X.unmop

@[simp]

theorem CategoryTheory.mop_hom_rightUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : Quiver.Hom.mop (CategoryTheory.MonoidalCategory.rightUnitor X).hom = (CategoryTheory.MonoidalCategory.leftUnitor { unmop := X }).hom

@[simp]

theorem CategoryTheory.unmop_hom_rightUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) : Quiver.Hom.unmop (CategoryTheory.MonoidalCategory.rightUnitor X).hom = (CategoryTheory.MonoidalCategory.leftUnitor X.unmop).hom

@[simp]

theorem CategoryTheory.mop_inv_rightUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : Quiver.Hom.mop (CategoryTheory.MonoidalCategory.rightUnitor X).inv = (CategoryTheory.MonoidalCategory.leftUnitor { unmop := X }).inv

@[simp]

theorem CategoryTheory.unmop_inv_rightUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) : Quiver.Hom.unmop (CategoryTheory.MonoidalCategory.rightUnitor X).inv = (CategoryTheory.MonoidalCategory.leftUnitor X.unmop).inv

@[simp]

theorem CategoryTheory.MonoidalOpposite.mopEquiv_counitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.MonoidalOpposite.mopEquiv C).counitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.comp (CategoryTheory.unmopFunctor C) (CategoryTheory.mopFunctor C))

@[simp]

theorem CategoryTheory.MonoidalOpposite.mopEquiv_unitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.MonoidalOpposite.mopEquiv C).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id C)

@[simp]

theorem CategoryTheory.MonoidalOpposite.mopEquiv_functor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.MonoidalOpposite.mopEquiv C).functor = CategoryTheory.mopFunctor C

@[simp]

theorem CategoryTheory.MonoidalOpposite.mopEquiv_inverse (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.MonoidalOpposite.mopEquiv C).inverse = CategoryTheory.unmopFunctor C

def CategoryTheory.MonoidalOpposite.mopEquiv (C : Type u₁) [CategoryTheory.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.

@[simp]

theorem CategoryTheory.MonoidalOpposite.unmopEquiv_unitIso_hom_app_unmop (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : Cᴹᵒᵖ) : ((CategoryTheory.MonoidalOpposite.unmopEquiv C).unitIso.hom.app X).unmop = CategoryTheory.CategoryStruct.id X.unmop

@[simp]

theorem CategoryTheory.MonoidalOpposite.unmopEquiv_functor_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (self : Cᴹᵒᵖ) : (CategoryTheory.MonoidalOpposite.unmopEquiv C).functor.obj self = self.unmop

@[simp]

theorem CategoryTheory.MonoidalOpposite.unmopEquiv_functor_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : ∀ {X Y : Cᴹᵒᵖ} (f : X ⟶ Y), (CategoryTheory.MonoidalOpposite.unmopEquiv C).functor.map f = Quiver.Hom.unmop f

@[simp]

theorem CategoryTheory.MonoidalOpposite.unmopEquiv_inverse_obj_unmop (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (unmop : C) : ((CategoryTheory.MonoidalOpposite.unmopEquiv C).inverse.obj unmop).unmop = unmop

@[simp]

theorem CategoryTheory.MonoidalOpposite.unmopEquiv_inverse_map_unmop (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : ∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.MonoidalOpposite.unmopEquiv C).inverse.map f).unmop = f

@[simp]

theorem CategoryTheory.MonoidalOpposite.unmopEquiv_counitIso_hom_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.MonoidalOpposite.unmopEquiv C).counitIso.hom.app X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.MonoidalOpposite.unmopEquiv_counitIso_inv_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.MonoidalOpposite.unmopEquiv C).counitIso.inv.app X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.MonoidalOpposite.unmopEquiv_unitIso_inv_app_unmop (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : Cᴹᵒᵖ) : ((CategoryTheory.MonoidalOpposite.unmopEquiv C).unitIso.inv.app X).unmop = CategoryTheory.CategoryStruct.id X.unmop

def CategoryTheory.MonoidalOpposite.unmopEquiv (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : Cᴹᵒᵖ ≌ C

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

Equations

• CategoryTheory.MonoidalOpposite.unmopEquiv C = (CategoryTheory.MonoidalOpposite.mopEquiv C).symm

@[simp]

theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_functor_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : ∀ {X Y : Cᴹᵒᵖᴹᵒᵖ} (f : X ⟶ Y), (CategoryTheory.MonoidalOpposite.mopMopEquivalence C).functor.map f = Quiver.Hom.unmop (Quiver.Hom.unmop f)

@[simp]

theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_counitIso_inv_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.MonoidalOpposite.mopMopEquivalence C).counitIso.inv.app X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_unitIso_inv_app_unmop_unmop (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : Cᴹᵒᵖᴹᵒᵖ) : ((CategoryTheory.MonoidalOpposite.mopMopEquivalence C).unitIso.inv.app X).unmop.unmop = (CategoryTheory.CategoryStruct.id X.unmop).unmop

@[simp]

theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_functor_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : Cᴹᵒᵖᴹᵒᵖ) : (CategoryTheory.MonoidalOpposite.mopMopEquivalence C).functor.obj X = X.unmop.unmop

@[simp]

theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_counitIso_hom_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.MonoidalOpposite.mopMopEquivalence C).counitIso.hom.app X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_inverse_map_unmop_unmop (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : ∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.MonoidalOpposite.mopMopEquivalence C).inverse.map f).unmop.unmop = f

@[simp]

theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_inverse_obj_unmop_unmop (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : ((CategoryTheory.MonoidalOpposite.mopMopEquivalence C).inverse.obj X).unmop.unmop = X

@[simp]

theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_unitIso_hom_app_unmop_unmop (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : Cᴹᵒᵖᴹᵒᵖ) : ((CategoryTheory.MonoidalOpposite.mopMopEquivalence C).unitIso.hom.app X).unmop.unmop = (CategoryTheory.CategoryStruct.id X.unmop).unmop

def CategoryTheory.MonoidalOpposite.mopMopEquivalence (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : Cᴹᵒᵖᴹᵒᵖ ≌ C

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

Equations

• CategoryTheory.MonoidalOpposite.mopMopEquivalence C = (CategoryTheory.MonoidalOpposite.unmopEquiv Cᴹᵒᵖ).trans (CategoryTheory.MonoidalOpposite.unmopEquiv C)

@[simp]

theorem CategoryTheory.MonoidalOpposite.tensorIso_hom_app_unmop (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ × Cᴹᵒᵖ) : ((CategoryTheory.MonoidalOpposite.tensorIso C).hom.app X).unmop = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X.2.unmop X.1.unmop)

@[simp]

theorem CategoryTheory.MonoidalOpposite.tensorIso_inv_app_unmop (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ × Cᴹᵒᵖ) : ((CategoryTheory.MonoidalOpposite.tensorIso C).inv.app X).unmop = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X.2.unmop X.1.unmop)

def CategoryTheory.MonoidalOpposite.tensorIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.MonoidalCategory.tensor Cᴹᵒᵖ ≅ CategoryTheory.Functor.comp (CategoryTheory.Functor.prod (CategoryTheory.unmopFunctor C) (CategoryTheory.unmopFunctor C)) (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap C C) (CategoryTheory.Functor.comp (CategoryTheory.MonoidalCategory.tensor C) (CategoryTheory.mopFunctor C)))

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

Equations

• CategoryTheory.MonoidalOpposite.tensorIso C = CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategory.tensor Cᴹᵒᵖ)

@[simp]

theorem CategoryTheory.MonoidalOpposite.tensorLeftIso_hom_app_unmop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) (X : Cᴹᵒᵖ) : ((CategoryTheory.MonoidalOpposite.tensorLeftIso X✝).hom.app X).unmop = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X.unmop X✝.unmop)

@[simp]

theorem CategoryTheory.MonoidalOpposite.tensorLeftIso_inv_app_unmop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) (X : Cᴹᵒᵖ) : ((CategoryTheory.MonoidalOpposite.tensorLeftIso X✝).inv.app X).unmop = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X.unmop X✝.unmop)

def CategoryTheory.MonoidalOpposite.tensorLeftIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) : CategoryTheory.MonoidalCategory.tensorLeft X ≅ CategoryTheory.Functor.comp (CategoryTheory.unmopFunctor C) (CategoryTheory.Functor.comp (CategoryTheory.MonoidalCategory.tensorRight X.unmop) (CategoryTheory.mopFunctor C))

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

Equations

• CategoryTheory.MonoidalOpposite.tensorLeftIso X = CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategory.tensorLeft X)

@[simp]

theorem CategoryTheory.MonoidalOpposite.tensorLeftMopIso_inv_app_unmop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (X : Cᴹᵒᵖ) : ((CategoryTheory.MonoidalOpposite.tensorLeftMopIso X✝).inv.app X).unmop = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X.unmop X✝)

@[simp]

theorem CategoryTheory.MonoidalOpposite.tensorLeftMopIso_hom_app_unmop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (X : Cᴹᵒᵖ) : ((CategoryTheory.MonoidalOpposite.tensorLeftMopIso X✝).hom.app X).unmop = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X.unmop X✝)

def CategoryTheory.MonoidalOpposite.tensorLeftMopIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : CategoryTheory.MonoidalCategory.tensorLeft { unmop := X } ≅ CategoryTheory.Functor.comp (CategoryTheory.unmopFunctor C) (CategoryTheory.Functor.comp (CategoryTheory.MonoidalCategory.tensorRight X) (CategoryTheory.mopFunctor C))

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

Equations

• CategoryTheory.MonoidalOpposite.tensorLeftMopIso X = CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategory.tensorLeft { unmop := X })

@[simp]

theorem CategoryTheory.MonoidalOpposite.tensorLeftUnmopIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) (X : C) : (CategoryTheory.MonoidalOpposite.tensorLeftUnmopIso X✝).hom.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X✝.unmop X)

@[simp]

theorem CategoryTheory.MonoidalOpposite.tensorLeftUnmopIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) (X : C) : (CategoryTheory.MonoidalOpposite.tensorLeftUnmopIso X✝).inv.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X✝.unmop X)

def CategoryTheory.MonoidalOpposite.tensorLeftUnmopIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) : CategoryTheory.MonoidalCategory.tensorLeft X.unmop ≅ CategoryTheory.Functor.comp (CategoryTheory.mopFunctor C) (CategoryTheory.Functor.comp (CategoryTheory.MonoidalCategory.tensorRight X) (CategoryTheory.unmopFunctor C))

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

Equations

• CategoryTheory.MonoidalOpposite.tensorLeftUnmopIso X = CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategory.tensorLeft X.unmop)

@[simp]

theorem CategoryTheory.MonoidalOpposite.tensorRightIso_inv_app_unmop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) (X : Cᴹᵒᵖ) : ((CategoryTheory.MonoidalOpposite.tensorRightIso X✝).inv.app X).unmop = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X✝.unmop X.unmop)

@[simp]

theorem CategoryTheory.MonoidalOpposite.tensorRightIso_hom_app_unmop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) (X : Cᴹᵒᵖ) : ((CategoryTheory.MonoidalOpposite.tensorRightIso X✝).hom.app X).unmop = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X✝.unmop X.unmop)

def CategoryTheory.MonoidalOpposite.tensorRightIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) : CategoryTheory.MonoidalCategory.tensorRight X ≅ CategoryTheory.Functor.comp (CategoryTheory.unmopFunctor C) (CategoryTheory.Functor.comp (CategoryTheory.MonoidalCategory.tensorLeft X.unmop) (CategoryTheory.mopFunctor C))

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

Equations

• CategoryTheory.MonoidalOpposite.tensorRightIso X = CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategory.tensorRight X)

@[simp]

theorem CategoryTheory.MonoidalOpposite.tensorRightMopIso_inv_app_unmop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (X : Cᴹᵒᵖ) : ((CategoryTheory.MonoidalOpposite.tensorRightMopIso X✝).inv.app X).unmop = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X✝ X.unmop)

@[simp]

theorem CategoryTheory.MonoidalOpposite.tensorRightMopIso_hom_app_unmop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (X : Cᴹᵒᵖ) : ((CategoryTheory.MonoidalOpposite.tensorRightMopIso X✝).hom.app X).unmop = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X✝ X.unmop)

def CategoryTheory.MonoidalOpposite.tensorRightMopIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : CategoryTheory.MonoidalCategory.tensorRight { unmop := X } ≅ CategoryTheory.Functor.comp (CategoryTheory.unmopFunctor C) (CategoryTheory.Functor.comp (CategoryTheory.MonoidalCategory.tensorLeft X) (CategoryTheory.mopFunctor C))

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

Equations

• CategoryTheory.MonoidalOpposite.tensorRightMopIso X = CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategory.tensorRight { unmop := X })

@[simp]

theorem CategoryTheory.MonoidalOpposite.tensorRightUnmopIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) (X : C) : (CategoryTheory.MonoidalOpposite.tensorRightUnmopIso X✝).hom.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X X✝.unmop)

@[simp]

theorem CategoryTheory.MonoidalOpposite.tensorRightUnmopIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) (X : C) : (CategoryTheory.MonoidalOpposite.tensorRightUnmopIso X✝).inv.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X X✝.unmop)

def CategoryTheory.MonoidalOpposite.tensorRightUnmopIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ) : CategoryTheory.MonoidalCategory.tensorRight X.unmop ≅ CategoryTheory.Functor.comp (CategoryTheory.mopFunctor C) (CategoryTheory.Functor.comp (CategoryTheory.MonoidalCategory.tensorLeft X) (CategoryTheory.unmopFunctor C))

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

Equations

• CategoryTheory.MonoidalOpposite.tensorRightUnmopIso X = CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategory.tensorRight X.unmop)