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: