Monoidal opposites

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

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

A type synonym for the monoidal opposite. Use the notation Cᴹᵒᵖ.

Equations

• Cᴹᵒᵖ = C

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

A type synonym for the monoidal opposite. Use the notation Cᴹᵒᵖ.

Equations

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

def CategoryTheory.MonoidalOpposite.mop {C : Type u₁} (X : C) : Cᴹᵒᵖ

Think of an object of C as an object of Cᴹᵒᵖ.

Equations

• CategoryTheory.MonoidalOpposite.mop X = X

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

Think of an object of Cᴹᵒᵖ as an object of C.

Equations

• CategoryTheory.MonoidalOpposite.unmop X = X

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.MonoidalOpposite.monoidalOppositeCategory = CategoryTheory.InducedCategory.category CategoryTheory.MonoidalOpposite.unmop

def Quiver.Hom.mop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.MonoidalOpposite.mop X ⟶ CategoryTheory.MonoidalOpposite.mop 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 = f

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

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

Equations

• Quiver.Hom.unmop f = f

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

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

@[simp]

theorem CategoryTheory.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 CategoryTheory.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 (CategoryTheory.MonoidalOpposite.mop 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 (CategoryTheory.MonoidalOpposite.unmop X)

@[simp]

theorem CategoryTheory.unmop_id_mop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : Quiver.Hom.unmop (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalOpposite.mop 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 (CategoryTheory.MonoidalOpposite.unmop X)) = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.Iso.mop_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ≅ Y) : (CategoryTheory.Iso.mop f).hom = Quiver.Hom.mop f.hom

@[simp]

theorem CategoryTheory.Iso.mop_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ≅ Y) : (CategoryTheory.Iso.mop f).inv = Quiver.Hom.mop f.inv

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

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

Equations

• CategoryTheory.Iso.mop f = CategoryTheory.Iso.mk (Quiver.Hom.mop f.hom) (Quiver.Hom.mop f.inv)

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

Equations

• CategoryTheory.monoidalCategoryOp = CategoryTheory.MonoidalCategory.mk

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

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

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

Equations

• CategoryTheory.monoidalCategoryMop = CategoryTheory.MonoidalCategory.mk

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

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