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.

Instances for CommMon_
theorem CommMon_.mul_comm_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (self : CommMon_ C) {X' : C} (f' : self.to_Mon_.X X') :
(β_ self.to_Mon_.X self.to_Mon_.X).hom self.to_Mon_.mul f' = self.to_Mon_.mul f'

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.

Instances for CommMon_.forget₂_Mon_

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.