mathlib3 documentation

category_theory.monoidal.CommMon_

The category of commutative monoids in a braided monoidal category. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A commutative monoid object internal to a monoidal category.

Instances for CommMon_
@[simp]

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

Equations
@[simp]

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.

Equations