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

• )
Instances For

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

Equations
Instances For
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
Equations
• CategoryTheory.MonoidalOpposite.monoidalOppositeCategory =
def Quiver.Hom.mop {C : Type u₁} [] {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
• f.mop = { unmop := f }
Instances For
def Quiver.Hom.unmop {C : Type u₁} [] {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
• f.unmop = f.unmop
Instances For
theorem Quiver.Hom.mop_inj {C : Type u₁} [] {X : C} {Y : C} :
Function.Injective Quiver.Hom.mop
theorem Quiver.Hom.unmop_inj {C : Type u₁} [] {X : Cᴹᵒᵖ} {Y : Cᴹᵒᵖ} :
Function.Injective Quiver.Hom.unmop
@[simp]
theorem Quiver.Hom.unmop_mop {C : Type u₁} [] {X : C} {Y : C} {f : X Y} :
f.mop.unmop = f
@[simp]
theorem Quiver.Hom.mop_unmop {C : Type u₁} [] {X : Cᴹᵒᵖ} {Y : Cᴹᵒᵖ} {f : X Y} :
f.unmop.mop = f
@[simp]
theorem CategoryTheory.mop_comp {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : X Y} {g : Y Z} :
@[simp]
theorem CategoryTheory.mop_id {C : Type u₁} [] {X : C} :
@[simp]
theorem CategoryTheory.unmop_comp {C : Type u₁} [] {X : Cᴹᵒᵖ} {Y : Cᴹᵒᵖ} {Z : Cᴹᵒᵖ} {f : X Y} {g : Y Z} :
.unmop = CategoryTheory.CategoryStruct.comp f.unmop g.unmop
@[simp]
theorem CategoryTheory.unmop_id {C : Type u₁} [] {X : Cᴹᵒᵖ} :
.unmop =
@[simp]
theorem CategoryTheory.unmop_id_mop {C : Type u₁} [] {X : C} :
(CategoryTheory.CategoryStruct.id { unmop := X }).unmop =
@[simp]
theorem CategoryTheory.mop_id_unmop {C : Type u₁} [] {X : Cᴹᵒᵖ} :
@[simp]
theorem CategoryTheory.mopFunctor_obj (C : Type u₁) [] (unmop : C) :
.obj unmop = { unmop := unmop }
@[simp]
theorem CategoryTheory.mopFunctor_map (C : Type u₁) [] :
∀ {X Y : C} (f : X Y), .map f = f.mop
def CategoryTheory.mopFunctor (C : Type u₁) [] :

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

Equations
• = { obj := CategoryTheory.MonoidalOpposite.mop, map := fun {X Y : C} => Quiver.Hom.mop, map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.unmopFunctor_map (C : Type u₁) [] :
∀ {X Y : Cᴹᵒᵖ} (f : X Y), .map f = f.unmop
@[simp]
theorem CategoryTheory.unmopFunctor_obj (C : Type u₁) [] (self : Cᴹᵒᵖ) :
.obj self = self.unmop
def CategoryTheory.unmopFunctor (C : Type u₁) [] :

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

Equations
• = { obj := CategoryTheory.MonoidalOpposite.unmop, map := fun {X Y : Cᴹᵒᵖ} => Quiver.Hom.unmop, map_id := , map_comp := }
Instances For
@[reducible, inline]
abbrev CategoryTheory.Iso.mop {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
{ unmop := X } { unmop := Y }

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

Equations
• f.mop = .mapIso f
Instances For
@[reducible, inline]
abbrev CategoryTheory.Iso.unmop {C : Type u₁} [] {X : Cᴹᵒᵖ} {Y : Cᴹᵒᵖ} (f : X Y) :
X.unmop Y.unmop

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

Equations
• f.unmop = .mapIso f
Instances For
instance CategoryTheory.IsIso.instMonoidalOppositeMop {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
Equations
• =
Equations
• =
Equations
@[simp]
theorem CategoryTheory.op_tensorObj {C : Type u₁} [] (X : C) (Y : C) :
@[simp]
theorem CategoryTheory.unop_tensorObj {C : Type u₁} [] (X : Cᵒᵖ) (Y : Cᵒᵖ) :
@[simp]
theorem CategoryTheory.op_tensorUnit {C : Type u₁} [] :
Opposite.op (𝟙_ C) = 𝟙_ Cᵒᵖ
@[simp]
theorem CategoryTheory.unop_tensorUnit {C : Type u₁} [] :
Opposite.unop (𝟙_ Cᵒᵖ) = 𝟙_ C
@[simp]
theorem CategoryTheory.op_tensorHom {C : Type u₁} [] {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} (f : X₁ Y₁) (g : X₂ Y₂) :
@[simp]
theorem CategoryTheory.unop_tensorHom {C : Type u₁} [] {X₁ : Cᵒᵖ} {Y₁ : Cᵒᵖ} {X₂ : Cᵒᵖ} {Y₂ : Cᵒᵖ} (f : X₁ Y₁) (g : X₂ Y₂) :
@[simp]
theorem CategoryTheory.op_whiskerLeft {C : Type u₁} [] (X : C) {Y : C} {Z : C} (f : Y Z) :
@[simp]
theorem CategoryTheory.unop_whiskerLeft {C : Type u₁} [] (X : Cᵒᵖ) {Y : Cᵒᵖ} {Z : Cᵒᵖ} (f : Y Z) :
@[simp]
theorem CategoryTheory.op_whiskerRight {C : Type u₁} [] {X : C} {Y : C} (f : X Y) (Z : C) :
@[simp]
theorem CategoryTheory.unop_whiskerRight {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) (Z : Cᵒᵖ) :
@[simp]
theorem CategoryTheory.op_associator {C : Type u₁} [] (X : C) (Y : C) (Z : C) :
.op = .symm
@[simp]
theorem CategoryTheory.unop_associator {C : Type u₁} [] (X : Cᵒᵖ) (Y : Cᵒᵖ) (Z : Cᵒᵖ) :
.unop = .symm
@[simp]
theorem CategoryTheory.op_hom_associator {C : Type u₁} [] (X : C) (Y : C) (Z : C) :
.hom.op = .inv
@[simp]
theorem CategoryTheory.unop_hom_associator {C : Type u₁} [] (X : Cᵒᵖ) (Y : Cᵒᵖ) (Z : Cᵒᵖ) :
.hom.unop = .inv
@[simp]
theorem CategoryTheory.op_inv_associator {C : Type u₁} [] (X : C) (Y : C) (Z : C) :
.inv.op = .hom
@[simp]
theorem CategoryTheory.unop_inv_associator {C : Type u₁} [] (X : Cᵒᵖ) (Y : Cᵒᵖ) (Z : Cᵒᵖ) :
.inv.unop = .hom
@[simp]
theorem CategoryTheory.op_leftUnitor {C : Type u₁} [] (X : C) :
@[simp]
theorem CategoryTheory.unop_leftUnitor {C : Type u₁} [] (X : Cᵒᵖ) :
@[simp]
theorem CategoryTheory.op_hom_leftUnitor {C : Type u₁} [] (X : C) :
@[simp]
theorem CategoryTheory.unop_hom_leftUnitor {C : Type u₁} [] (X : Cᵒᵖ) :
@[simp]
theorem CategoryTheory.op_inv_leftUnitor {C : Type u₁} [] (X : C) :
@[simp]
theorem CategoryTheory.unop_inv_leftUnitor {C : Type u₁} [] (X : Cᵒᵖ) :
@[simp]
theorem CategoryTheory.op_rightUnitor {C : Type u₁} [] (X : C) :
@[simp]
theorem CategoryTheory.unop_rightUnitor {C : Type u₁} [] (X : Cᵒᵖ) :
@[simp]
theorem CategoryTheory.op_hom_rightUnitor {C : Type u₁} [] (X : C) :
@[simp]
theorem CategoryTheory.unop_hom_rightUnitor {C : Type u₁} [] (X : Cᵒᵖ) :
@[simp]
theorem CategoryTheory.op_inv_rightUnitor {C : Type u₁} [] (X : C) :
@[simp]
theorem CategoryTheory.unop_inv_rightUnitor {C : Type u₁} [] (X : Cᵒᵖ) :
theorem CategoryTheory.op_tensor_op {C : Type u₁} [] {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : Y Z) :
theorem CategoryTheory.unop_tensor_unop {C : Type u₁} [] {W : Cᵒᵖ} {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} (f : W X) (g : Y Z) :
Equations
@[simp]
theorem CategoryTheory.mop_tensorObj {C : Type u₁} [] (X : C) (Y : C) :
{ unmop := } = CategoryTheory.MonoidalCategory.tensorObj { unmop := Y } { unmop := X }
@[simp]
theorem CategoryTheory.unmop_tensorObj {C : Type u₁} [] (X : Cᴹᵒᵖ) (Y : Cᴹᵒᵖ) :
@[simp]
theorem CategoryTheory.mop_tensorUnit {C : Type u₁} [] :
{ unmop := 𝟙_ C } = 𝟙_ Cᴹᵒᵖ
@[simp]
theorem CategoryTheory.unmop_tensorUnit {C : Type u₁} [] :
(𝟙_ Cᴹᵒᵖ).unmop = 𝟙_ C
@[simp]
theorem CategoryTheory.mop_tensorHom {C : Type u₁} [] {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} (f : X₁ Y₁) (g : X₂ Y₂) :
=
@[simp]
theorem CategoryTheory.unmop_tensorHom {C : Type u₁} [] {X₁ : Cᴹᵒᵖ} {Y₁ : Cᴹᵒᵖ} {X₂ : Cᴹᵒᵖ} {Y₂ : Cᴹᵒᵖ} (f : X₁ Y₁) (g : X₂ Y₂) :
@[simp]
theorem CategoryTheory.mop_whiskerLeft {C : Type u₁} [] (X : C) {Y : C} {Z : C} (f : Y Z) :
@[simp]
theorem CategoryTheory.unmop_whiskerLeft {C : Type u₁} [] (X : Cᴹᵒᵖ) {Y : Cᴹᵒᵖ} {Z : Cᴹᵒᵖ} (f : Y Z) :
@[simp]
theorem CategoryTheory.mop_whiskerRight {C : Type u₁} [] {X : C} {Y : C} (f : X Y) (Z : C) :
@[simp]
theorem CategoryTheory.unmop_whiskerRight {C : Type u₁} [] {X : Cᴹᵒᵖ} {Y : Cᴹᵒᵖ} (f : X Y) (Z : Cᴹᵒᵖ) :
@[simp]
theorem CategoryTheory.mop_associator {C : Type u₁} [] (X : C) (Y : C) (Z : C) :
.mop = (CategoryTheory.MonoidalCategory.associator { unmop := Z } { unmop := Y } { unmop := X }).symm
@[simp]
theorem CategoryTheory.unmop_associator {C : Type u₁} [] (X : Cᴹᵒᵖ) (Y : Cᴹᵒᵖ) (Z : Cᴹᵒᵖ) :
.unmop = (CategoryTheory.MonoidalCategory.associator Z.unmop Y.unmop X.unmop).symm
@[simp]
theorem CategoryTheory.mop_hom_associator {C : Type u₁} [] (X : C) (Y : C) (Z : C) :
.hom.mop = (CategoryTheory.MonoidalCategory.associator { unmop := Z } { unmop := Y } { unmop := X }).inv
@[simp]
theorem CategoryTheory.unmop_hom_associator {C : Type u₁} [] (X : Cᴹᵒᵖ) (Y : Cᴹᵒᵖ) (Z : Cᴹᵒᵖ) :
.hom.unmop = (CategoryTheory.MonoidalCategory.associator Z.unmop Y.unmop X.unmop).inv
@[simp]
theorem CategoryTheory.mop_inv_associator {C : Type u₁} [] (X : C) (Y : C) (Z : C) :
.inv.mop = (CategoryTheory.MonoidalCategory.associator { unmop := Z } { unmop := Y } { unmop := X }).hom
@[simp]
theorem CategoryTheory.unmop_inv_associator {C : Type u₁} [] (X : Cᴹᵒᵖ) (Y : Cᴹᵒᵖ) (Z : Cᴹᵒᵖ) :
.inv.unmop = (CategoryTheory.MonoidalCategory.associator Z.unmop Y.unmop X.unmop).hom
@[simp]
@[simp]
theorem CategoryTheory.unmop_leftUnitor {C : Type u₁} [] (X : Cᴹᵒᵖ) :
@[simp]
theorem CategoryTheory.mop_hom_leftUnitor {C : Type u₁} [] (X : C) :
@[simp]
theorem CategoryTheory.unmop_hom_leftUnitor {C : Type u₁} [] (X : Cᴹᵒᵖ) :
.unmop = .hom
@[simp]
theorem CategoryTheory.mop_inv_leftUnitor {C : Type u₁} [] (X : C) :
@[simp]
theorem CategoryTheory.unmop_inv_leftUnitor {C : Type u₁} [] (X : Cᴹᵒᵖ) :
.unmop = .inv
@[simp]
@[simp]
theorem CategoryTheory.unmop_rightUnitor {C : Type u₁} [] (X : Cᴹᵒᵖ) :
@[simp]
theorem CategoryTheory.mop_hom_rightUnitor {C : Type u₁} [] (X : C) :
@[simp]
theorem CategoryTheory.unmop_hom_rightUnitor {C : Type u₁} [] (X : Cᴹᵒᵖ) :
.unmop = .hom
@[simp]
theorem CategoryTheory.mop_inv_rightUnitor {C : Type u₁} [] (X : C) :
@[simp]
theorem CategoryTheory.unmop_inv_rightUnitor {C : Type u₁} [] (X : Cᴹᵒᵖ) :
.unmop = .inv
@[simp]
theorem CategoryTheory.MonoidalOpposite.mopEquiv_counitIso (C : Type u₁) [] :
.counitIso =

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.MonoidalOpposite.unmopEquiv_unitIso_inv_app_unmop (C : Type u₁) [] (X : Cᴹᵒᵖ) :
(.unitIso.inv.app X).unmop =
@[simp]
theorem CategoryTheory.MonoidalOpposite.unmopEquiv_inverse_obj_unmop (C : Type u₁) [] (unmop : C) :
(.inverse.obj unmop).unmop = unmop
@[simp]
theorem CategoryTheory.MonoidalOpposite.unmopEquiv_functor_obj (C : Type u₁) [] (self : Cᴹᵒᵖ) :
.functor.obj self = self.unmop
@[simp]
theorem CategoryTheory.MonoidalOpposite.unmopEquiv_unitIso_hom_app_unmop (C : Type u₁) [] (X : Cᴹᵒᵖ) :
(.unitIso.hom.app X).unmop =
@[simp]
theorem CategoryTheory.MonoidalOpposite.unmopEquiv_counitIso_inv_app (C : Type u₁) [] (X : C) :
.counitIso.inv.app X =
@[simp]
theorem CategoryTheory.MonoidalOpposite.unmopEquiv_inverse_map_unmop (C : Type u₁) [] :
∀ {X Y : C} (f : X Y), (.inverse.map f).unmop = f
@[simp]
theorem CategoryTheory.MonoidalOpposite.unmopEquiv_functor_map (C : Type u₁) [] :
∀ {X Y : Cᴹᵒᵖ} (f : X Y), .functor.map f = f.unmop
@[simp]
theorem CategoryTheory.MonoidalOpposite.unmopEquiv_counitIso_hom_app (C : Type u₁) [] (X : C) :
.counitIso.hom.app X =

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

Equations
Instances For
@[simp]
theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_counitIso_hom_app (C : Type u₁) [] (X : C) :
.counitIso.hom.app X =
@[simp]
@[simp]
@[simp]
theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_functor_map (C : Type u₁) [] :
∀ {X Y : } (f : X Y), .map f = f.unmop.unmop
@[simp]
theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_counitIso_inv_app (C : Type u₁) [] (X : C) :
.counitIso.inv.app X =
@[simp]
theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_inverse_map_unmop_unmop (C : Type u₁) [] :
∀ {X Y : C} (f : X Y), (.map f).unmop.unmop = f
@[simp]
theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_inverse_obj_unmop_unmop (C : Type u₁) [] (X : C) :
(.obj X).unmop.unmop = X
@[simp]
theorem CategoryTheory.MonoidalOpposite.mopMopEquivalence_functor_obj (C : Type u₁) [] (X : ) :
.obj X = X.unmop.unmop

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

Equations
Instances For
def CategoryTheory.MonoidalOpposite.tensorIso (C : Type u₁) [] :
(.prod ).comp (.comp )

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

Equations
Instances For
@[simp]
@[simp]
def CategoryTheory.MonoidalOpposite.tensorLeftIso {C : Type u₁} [] (X : Cᴹᵒᵖ) :
.comp (.comp )

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

Equations
• X.tensorLeftIso =
Instances For
@[simp]
theorem CategoryTheory.MonoidalOpposite.tensorLeftMopIso_hom_app_unmop {C : Type u₁} [] (X : C) (X : Cᴹᵒᵖ) :
(.app X).unmop =
@[simp]
theorem CategoryTheory.MonoidalOpposite.tensorLeftMopIso_inv_app_unmop {C : Type u₁} [] (X : C) (X : Cᴹᵒᵖ) :
(.app X).unmop =

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

Equations
Instances For
@[simp]
theorem CategoryTheory.MonoidalOpposite.tensorLeftUnmopIso_inv_app {C : Type u₁} [] (X : Cᴹᵒᵖ) (X : C) :
X✝.tensorLeftUnmopIso.inv.app X =
@[simp]
theorem CategoryTheory.MonoidalOpposite.tensorLeftUnmopIso_hom_app {C : Type u₁} [] (X : Cᴹᵒᵖ) (X : C) :
X✝.tensorLeftUnmopIso.hom.app X =

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

Equations
• X.tensorLeftUnmopIso =
Instances For
@[simp]
@[simp]
def CategoryTheory.MonoidalOpposite.tensorRightIso {C : Type u₁} [] (X : Cᴹᵒᵖ) :
.comp (.comp )

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

Equations
• X.tensorRightIso =
Instances For
@[simp]
theorem CategoryTheory.MonoidalOpposite.tensorRightMopIso_inv_app_unmop {C : Type u₁} [] (X : C) (X : Cᴹᵒᵖ) :
(.app X).unmop =
@[simp]
theorem CategoryTheory.MonoidalOpposite.tensorRightMopIso_hom_app_unmop {C : Type u₁} [] (X : C) (X : Cᴹᵒᵖ) :
(.app X).unmop =

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

Equations
Instances For
@[simp]
theorem CategoryTheory.MonoidalOpposite.tensorRightUnmopIso_inv_app {C : Type u₁} [] (X : Cᴹᵒᵖ) (X : C) :
X✝.tensorRightUnmopIso.inv.app X =
@[simp]
theorem CategoryTheory.MonoidalOpposite.tensorRightUnmopIso_hom_app {C : Type u₁} [] (X : Cᴹᵒᵖ) (X : C) :
X✝.tensorRightUnmopIso.hom.app X =

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

Equations
• X.tensorRightUnmopIso =
Instances For