mathlib documentation


The category of commutative monoids in a braided monoidal category.

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

A commutative monoid object internal to a monoidal category.

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

theorem CommMon_.comp_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {R S T : CommMon_ C} (f : R S) (g : S T) :
(f g).hom = f.hom g.hom

The forgetful functor from commutative monoid objects to monoid objects.


A lax braided functor takes commutative monoid objects to commutative monoid objects.

That is, a lax braided functor F : C ⥤ D induces a functor CommMon_ C ⥤ CommMon_ D.