mathlib documentation

category_theory.monoidal.opposite

Monoidal opposites #

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

@[nolint]
def category_theory.monoidal_opposite (C : Type u₁) :
Type u₁

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

Equations
def category_theory.monoidal_opposite.mop {C : Type u₁} (X : C) :

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

Equations
def category_theory.monoidal_opposite.unmop {C : Type u₁} (X : Cᴹᵒᵖ) :
C

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

Equations

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

Equations

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

Equations
@[simp]
theorem category_theory.unmop_mop {C : Type u₁} [category_theory.category C] {X Y : C} {f : X Y} :
f.mop.unmop = f
@[simp]
theorem category_theory.mop_unmop {C : Type u₁} [category_theory.category C] {X Y : Cᴹᵒᵖ} {f : X Y} :
f.unmop.mop = f
@[simp]
theorem category_theory.mop_comp {C : Type u₁} [category_theory.category C] {X Y Z : C} {f : X Y} {g : Y Z} :
(f g).mop = f.mop g.mop
@[simp]
theorem category_theory.unmop_comp {C : Type u₁} [category_theory.category C] {X Y Z : Cᴹᵒᵖ} {f : X Y} {g : Y Z} :
(f g).unmop = f.unmop g.unmop

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

Equations
@[simp]
theorem category_theory.iso.mop_inv {C : Type u₁} [category_theory.category C] {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.iso.mop_hom {C : Type u₁} [category_theory.category C] {X Y : C} (f : X Y) :