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 mop

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

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

@[simp]

theorem CategoryTheory.MonoidalOpposite.unmop_inj_iff {C : Type u₁} (x 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₁} [Category.{v₁, u₁} C] : Category.{v₁, u₁} Cᴹᵒᵖ

Equations

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

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

• f.mop = { unmop := f }

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

• f.unmop = f.unmop

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

Equations

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

@[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)

@[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)

@[simp]

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

@[simp]

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

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

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

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

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

@[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)

@[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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Equations

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

@[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 }

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

@[simp]

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

@[simp]

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

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

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

@[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 }

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.MonoidalOpposite.unmopEquiv (C : Type u₁) [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.unmopEquiv_counitIso_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (X : C) : (unmopEquiv C).counitIso.inv.app X = CategoryStruct.id X

@[simp]

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

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

@[simp]

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

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

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

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

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

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

@[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)

@[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)

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

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

@[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)

@[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)

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

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

@[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)

@[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)

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

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

@[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✝)

@[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✝)

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

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

@[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)

@[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)

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

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

@[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)

@[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)

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

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

@[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)

@[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)