mathlib docs: category_theory.monoidal.discrete

source

@[instance]

def category_theory.monoid_discrete (M : Type u) [monoid M] :

monoid (category_theory.discrete M)

Equations

category_theory.monoid_discrete M = id _inst_1

source

@[instance]

def category_theory.category_theory.monoidal_category (M : Type u) [monoid M] :

category_theory.monoidal_category (category_theory.discrete M)

Equations

category_theory.category_theory.monoidal_category M = {tensor_obj := λ (X Y : category_theory.discrete M), X * Y, tensor_hom := λ (W X Y Z : category_theory.discrete M) (f : W ⟶ X) (g : Y ⟶ Z), category_theory.eq_to_hom _, tensor_id' := _, tensor_comp' := _, tensor_unit := 1, associator := λ (X Y Z : category_theory.discrete M), category_theory.eq_to_iso _, associator_naturality' := _, left_unitor := λ (X : category_theory.discrete M), category_theory.eq_to_iso _, left_unitor_naturality' := _, right_unitor := λ (X : category_theory.discrete M), category_theory.eq_to_iso _, right_unitor_naturality' := _, pentagon' := _, triangle' := _}

source

@[simp]

theorem category_theory.discrete.monoidal_functor_ε_is_iso {M : Type u} [monoid M] {N : Type u} [monoid N] (F : M →* N) :

(category_theory.discrete.monoidal_functor F).ε_is_iso = category_theory.discrete.category_theory.is_iso {to_functor := {obj := ⇑F, map := λ (X Y : category_theory.discrete M) (f : X ⟶ Y), category_theory.eq_to_hom _, map_id' := _, map_comp' := _}, ε := category_theory.eq_to_hom _, μ := λ (X Y : category_theory.discrete M), category_theory.eq_to_hom _, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}.ε

source

def category_theory.discrete.monoidal_functor {M : Type u} [monoid M] {N : Type u} [monoid N] (F : M →* N) :

category_theory.monoidal_functor (category_theory.discrete M) (category_theory.discrete N)

A multiplicative morphism between monoids gives a monoidal functor between the corresponding discrete monoidal categories.

Equations

category_theory.discrete.monoidal_functor F = {to_lax_monoidal_functor := {to_functor := {obj := ⇑F, map := λ (X Y : category_theory.discrete M) (f : X ⟶ Y), category_theory.eq_to_hom _, map_id' := _, map_comp' := _}, ε := category_theory.eq_to_hom _, μ := λ (X Y : category_theory.discrete M), category_theory.eq_to_hom _, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, ε_is_iso := category_theory.discrete.category_theory.is_iso {to_functor := {obj := ⇑F, map := λ (X Y : category_theory.discrete M) (f : X ⟶ Y), category_theory.eq_to_hom _, map_id' := _, map_comp' := _}, ε := category_theory.eq_to_hom _, μ := λ (X Y : category_theory.discrete M), category_theory.eq_to_hom _, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}.ε, μ_is_iso := λ (X Y : category_theory.discrete M), category_theory.discrete.category_theory.is_iso ({to_functor := {obj := ⇑F, map := λ (X Y : category_theory.discrete M) (f : X ⟶ Y), category_theory.eq_to_hom _, map_id' := _, map_comp' := _}, ε := category_theory.eq_to_hom _, μ := λ (X Y : category_theory.discrete M), category_theory.eq_to_hom _, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}.μ X Y)}

source

@[simp]

theorem category_theory.discrete.monoidal_functor_to_lax_monoidal_functor_μ {M : Type u} [monoid M] {N : Type u} [monoid N] (F : M →* N) (X Y : category_theory.discrete M) :

(category_theory.discrete.monoidal_functor F).to_lax_monoidal_functor.μ X Y = category_theory.eq_to_hom _

source

@[simp]

theorem category_theory.discrete.monoidal_functor_to_lax_monoidal_functor_to_functor_obj {M : Type u} [monoid M] {N : Type u} [monoid N] (F : M →* N) (a : M) :

(category_theory.discrete.monoidal_functor F).to_lax_monoidal_functor.to_functor.obj a = ⇑F a

source

@[simp]

theorem category_theory.discrete.monoidal_functor_μ_is_iso {M : Type u} [monoid M] {N : Type u} [monoid N] (F : M →* N) (X Y : category_theory.discrete M) :

(category_theory.discrete.monoidal_functor F).μ_is_iso X Y = category_theory.discrete.category_theory.is_iso ({to_functor := {obj := ⇑F, map := λ (X Y : category_theory.discrete M) (f : X ⟶ Y), category_theory.eq_to_hom _, map_id' := _, map_comp' := _}, ε := category_theory.eq_to_hom _, μ := λ (X Y : category_theory.discrete M), category_theory.eq_to_hom _, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}.μ X Y)

source

@[simp]

theorem category_theory.discrete.monoidal_functor_to_lax_monoidal_functor_ε {M : Type u} [monoid M] {N : Type u} [monoid N] (F : M →* N) :

(category_theory.discrete.monoidal_functor F).to_lax_monoidal_functor.ε = category_theory.eq_to_hom _

source

@[simp]

theorem category_theory.discrete.monoidal_functor_to_lax_monoidal_functor_to_functor_map {M : Type u} [monoid M] {N : Type u} [monoid N] (F : M →* N) (X Y : category_theory.discrete M) (f : X ⟶ Y) :

(category_theory.discrete.monoidal_functor F).to_lax_monoidal_functor.to_functor.map f = category_theory.eq_to_hom _

source

def category_theory.discrete.monoidal_functor_comp {M : Type u} [monoid M] {N : Type u} [monoid N] {K : Type u} [monoid K] (F : M →* N) (G : N →* K) :

category_theory.discrete.monoidal_functor F ⊗⋙ category_theory.discrete.monoidal_functor G ≅ category_theory.discrete.monoidal_functor (G.comp F)

The monoidal natural isomorphism corresponding to composing two multiplicative morphisms.

Equations

category_theory.discrete.monoidal_functor_comp F G = {hom := {to_nat_trans := {app := λ (X : category_theory.discrete M), 𝟙 ((category_theory.discrete.monoidal_functor F ⊗⋙ category_theory.discrete.monoidal_functor G).to_lax_monoidal_functor.to_functor.obj X), naturality' := _}, unit' := _, tensor' := _}, inv := {to_nat_trans := {app := λ (X : category_theory.discrete M), 𝟙 ((category_theory.discrete.monoidal_functor (G.comp F)).to_lax_monoidal_functor.to_functor.obj X), naturality' := _}, unit' := _, tensor' := _}, hom_inv_id' := _, inv_hom_id' := _}

mathlib documentation

Monoids as discrete monoidal categories