mathlib documentation

category_theory.monoidal.Mon_

The category of monoids in a monoidal category. #

structure Mon_ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :
Type (max u₁ v₁)

A monoid object internal to a monoidal category.

When the monoidal category is preadditive, this is also sometimes called an "algebra object".

theorem Mon_.one_mul {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (c : Mon_ C) :
(c.one 𝟙 c.X) c.mul = (λ_ c.X).hom
theorem Mon_.mul_one {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (c : Mon_ C) :
(𝟙 c.X c.one) c.mul = (ρ_ c.X).hom
@[simp]
theorem Mon_.mul_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (c : Mon_ C) :
(c.mul 𝟙 c.X) c.mul = (α_ c.X c.X c.X).hom (𝟙 c.X c.mul) c.mul
theorem Mon_.one_mul_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (c : Mon_ C) {X' : C} (f' : c.X X') :
(c.one 𝟙 c.X) c.mul f' = (λ_ c.X).hom f'
theorem Mon_.mul_one_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (c : Mon_ C) {X' : C} (f' : c.X X') :
(𝟙 c.X c.one) c.mul f' = (ρ_ c.X).hom f'
@[simp]
theorem Mon_.mul_assoc_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (c : Mon_ C) {X' : C} (f' : c.X X') :
(c.mul 𝟙 c.X) c.mul f' = (α_ c.X c.X c.X).hom (𝟙 c.X c.mul) c.mul f'

The trivial monoid object. We later show this is initial in Mon_ C.

Equations
@[instance]
Equations
@[simp]
theorem Mon_.one_mul_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {M : Mon_ C} {Z : C} (f : Z M.X) :
(M.one f) M.mul = (λ_ Z).hom f
@[simp]
theorem Mon_.mul_one_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {M : Mon_ C} {Z : C} (f : Z M.X) :
(f M.one) M.mul = (ρ_ Z).hom f
theorem Mon_.assoc_flip {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {M : Mon_ C} :
(𝟙 M.X M.mul) M.mul = (α_ M.X M.X M.X).inv (M.mul 𝟙 M.X) M.mul
theorem Mon_.hom.ext_iff {C : Type u₁} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.monoidal_category C} {M N : Mon_ C} (x y : M.hom N) :
x = y x.hom = y.hom
@[ext]
structure Mon_.hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (M N : Mon_ C) :
Type v₁

A morphism of monoid objects.

theorem Mon_.hom.ext {C : Type u₁} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.monoidal_category C} {M N : Mon_ C} (x y : M.hom N) (h : x.hom = y.hom) :
x = y
@[simp]
theorem Mon_.hom.one_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {M N : Mon_ C} (c : M.hom N) :
M.one c.hom = N.one
@[simp]
theorem Mon_.hom.mul_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {M N : Mon_ C} (c : M.hom N) :
M.mul c.hom = (c.hom c.hom) N.mul
@[simp]
theorem Mon_.hom.mul_hom_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {M N : Mon_ C} (c : M.hom N) {X' : C} (f' : N.X X') :
M.mul c.hom f' = (c.hom c.hom) N.mul f'
@[simp]
theorem Mon_.hom.one_hom_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {M N : Mon_ C} (c : M.hom N) {X' : C} (f' : N.X X') :
M.one c.hom f' = N.one f'
def Mon_.id {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (M : Mon_ C) :
M.hom M

The identity morphism on a monoid object.

Equations
@[simp]
theorem Mon_.id_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (M : Mon_ C) :
M.id.hom = 𝟙 M.X
@[instance]
Equations
def Mon_.comp {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {M N O : Mon_ C} (f : M.hom N) (g : N.hom O) :
M.hom O

Composition of morphisms of monoid objects.

Equations
@[simp]
theorem Mon_.comp_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {M N O : Mon_ C} (f : M.hom N) (g : N.hom O) :
(Mon_.comp f g).hom = f.hom g.hom
@[instance]
Equations
@[simp]
theorem Mon_.id_hom' {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (M : Mon_ C) :
(𝟙 M).hom = 𝟙 M.X
@[simp]
theorem Mon_.comp_hom' {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {M N K : Mon_ C} (f : M N) (g : N K) :
(f g).hom = f.hom g.hom
@[simp]
@[simp]
theorem Mon_.forget_map (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (A B : Mon_ C) (f : A B) :

The forgetful functor from monoid objects to the ambient category.

Equations

A lax monoidal functor takes monoid objects to monoid objects.

That is, a lax monoidal functor F : C ⥤ D induces a functor Mon_ C ⥤ Mon_ D.

Equations

Projects: