category_theory.monoidal.opposite

source

@[nolint, irreducible]

def category_theory.monoidal_opposite (C : Type u₁) :

Type u₁

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

Equations

Cᴹᵒᵖ = C

Instances for category_theory.monoidal_opposite

source

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

Cᴹᵒᵖ

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

Equations

category_theory.monoidal_opposite.mop X = X

source

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

C

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

Equations

category_theory.monoidal_opposite.unmop X = X

source

theorem category_theory.monoidal_opposite.op_injective {C : Type u₁} :

function.injective category_theory.monoidal_opposite.mop

source

theorem category_theory.monoidal_opposite.unop_injective {C : Type u₁} :

function.injective category_theory.monoidal_opposite.unmop

source

@[simp]

theorem category_theory.monoidal_opposite.op_inj_iff {C : Type u₁} (x y : C) :

category_theory.monoidal_opposite.mop x = category_theory.monoidal_opposite.mop y ↔ x = y

source

@[simp]

theorem category_theory.monoidal_opposite.unop_inj_iff {C : Type u₁} (x y : Cᴹᵒᵖ) :

category_theory.monoidal_opposite.unmop x = category_theory.monoidal_opposite.unmop y ↔ x = y

source

@[simp]

theorem category_theory.monoidal_opposite.mop_unmop {C : Type u₁} (X : Cᴹᵒᵖ) :

category_theory.monoidal_opposite.mop (category_theory.monoidal_opposite.unmop X) = X

source

@[simp]

theorem category_theory.monoidal_opposite.unmop_mop {C : Type u₁} (X : C) :

category_theory.monoidal_opposite.unmop (category_theory.monoidal_opposite.mop X) = X

source

@[protected, instance]

def category_theory.monoidal_opposite.monoidal_opposite_category {C : Type u₁} [I : category_theory.category C] :

category_theory.category Cᴹᵒᵖ

Equations

category_theory.monoidal_opposite.monoidal_opposite_category = {to_category_struct := {to_quiver := {hom := λ (X Y : Cᴹᵒᵖ), category_theory.monoidal_opposite.unmop X ⟶ category_theory.monoidal_opposite.unmop Y}, id := λ (X : Cᴹᵒᵖ), 𝟙 (category_theory.monoidal_opposite.unmop X), comp := λ (X Y Z : Cᴹᵒᵖ) (f : X ⟶ Y) (g : Y ⟶ Z), f ≫ g}, id_comp' := _, comp_id' := _, assoc' := _}

source

def quiver.hom.mop {C : Type u₁} [category_theory.category C] {X Y : C} (f : X ⟶ Y) :

category_theory.monoidal_opposite.mop X ⟶ category_theory.monoidal_opposite.mop Y

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

Equations

f.mop = f

source

def quiver.hom.unmop {C : Type u₁} [category_theory.category C] {X Y : Cᴹᵒᵖ} (f : X ⟶ Y) :

category_theory.monoidal_opposite.unmop X ⟶ category_theory.monoidal_opposite.unmop Y

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

Equations

f.unmop = f

source

theorem category_theory.mop_inj {C : Type u₁} [category_theory.category C] {X Y : C} :

function.injective quiver.hom.mop

source

theorem category_theory.unmop_inj {C : Type u₁} [category_theory.category C] {X Y : Cᴹᵒᵖ} :

function.injective quiver.hom.unmop

source

@[simp]

theorem category_theory.unmop_mop {C : Type u₁} [category_theory.category C] {X Y : C} {f : X ⟶ Y} :

f.mop.unmop = f

source

@[simp]

theorem category_theory.mop_unmop {C : Type u₁} [category_theory.category C] {X Y : Cᴹᵒᵖ} {f : X ⟶ Y} :

f.unmop.mop = f

source

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

source

@[simp]

theorem category_theory.mop_id {C : Type u₁} [category_theory.category C] {X : C} :

(𝟙 X).mop = 𝟙 (category_theory.monoidal_opposite.mop X)

source

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

source

@[simp]

theorem category_theory.unmop_id {C : Type u₁} [category_theory.category C] {X : Cᴹᵒᵖ} :

(𝟙 X).unmop = 𝟙 (category_theory.monoidal_opposite.unmop X)

source

@[simp]

theorem category_theory.unmop_id_mop {C : Type u₁} [category_theory.category C] {X : C} :

(𝟙 (category_theory.monoidal_opposite.mop X)).unmop = 𝟙 X

source

@[simp]

theorem category_theory.mop_id_unmop {C : Type u₁} [category_theory.category C] {X : Cᴹᵒᵖ} :

(𝟙 (category_theory.monoidal_opposite.unmop X)).mop = 𝟙 X

source

def category_theory.iso.mop {C : Type u₁} [category_theory.category C] {X Y : C} (f : X ≅ Y) :

category_theory.monoidal_opposite.mop X ≅ category_theory.monoidal_opposite.mop Y

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

Equations

f.mop = {hom := f.hom.mop, inv := f.inv.mop, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

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

f.mop.inv = f.inv.mop

source

@[simp]

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

f.mop.hom = f.hom.mop

source

@[protected, instance]

def category_theory.monoidal_category_op {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.monoidal_category Cᵒᵖ

Equations

category_theory.monoidal_category_op = {tensor_obj := λ (X Y : Cᵒᵖ), opposite.op (opposite.unop X ⊗ opposite.unop Y), tensor_hom := λ (X₁ Y₁ X₂ Y₂ : Cᵒᵖ) (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), (f.unop ⊗ g.unop).op, tensor_id' := _, tensor_comp' := _, tensor_unit := opposite.op (𝟙_ C), associator := λ (X Y Z : Cᵒᵖ), (α_ (opposite.unop X) (opposite.unop Y) (opposite.unop Z)).symm.op, associator_naturality' := _, left_unitor := λ (X : Cᵒᵖ), (λ_ (opposite.unop X)).symm.op, left_unitor_naturality' := _, right_unitor := λ (X : Cᵒᵖ), (ρ_ (opposite.unop X)).symm.op, right_unitor_naturality' := _, pentagon' := _, triangle' := _}

source

theorem category_theory.op_tensor_obj {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X Y : Cᵒᵖ) :

X ⊗ Y = opposite.op (opposite.unop X ⊗ opposite.unop Y)

source

theorem category_theory.op_tensor_unit {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] :

𝟙_ Cᵒᵖ = opposite.op (𝟙_ C)

source

@[protected, instance]

def category_theory.monoidal_category_mop {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.monoidal_category Cᴹᵒᵖ

Equations

category_theory.monoidal_category_mop = {tensor_obj := λ (X Y : Cᴹᵒᵖ), category_theory.monoidal_opposite.mop (category_theory.monoidal_opposite.unmop Y ⊗ category_theory.monoidal_opposite.unmop X), tensor_hom := λ (X₁ Y₁ X₂ Y₂ : Cᴹᵒᵖ) (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), (g.unmop ⊗ f.unmop).mop, tensor_id' := _, tensor_comp' := _, tensor_unit := category_theory.monoidal_opposite.mop (𝟙_ C), associator := λ (X Y Z : Cᴹᵒᵖ), (α_ (category_theory.monoidal_opposite.unmop Z) (category_theory.monoidal_opposite.unmop Y) (category_theory.monoidal_opposite.unmop X)).symm.mop, associator_naturality' := _, left_unitor := λ (X : Cᴹᵒᵖ), (ρ_ (category_theory.monoidal_opposite.unmop X)).mop, left_unitor_naturality' := _, right_unitor := λ (X : Cᴹᵒᵖ), (λ_ (category_theory.monoidal_opposite.unmop X)).mop, right_unitor_naturality' := _, pentagon' := _, triangle' := _}

source

theorem category_theory.mop_tensor_obj {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X Y : Cᴹᵒᵖ) :

X ⊗ Y = category_theory.monoidal_opposite.mop (category_theory.monoidal_opposite.unmop Y ⊗ category_theory.monoidal_opposite.unmop X)

source

theorem category_theory.mop_tensor_unit {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] :

𝟙_ Cᴹᵒᵖ = category_theory.monoidal_opposite.mop (𝟙_ C)

mathlib3 documentation

Monoidal opposites #