The category of commutative monoids in a braided monoidal category. #
- X : C
- one : CategoryTheory.MonoidalCategory.tensorUnit C ⟶ s.X
- mul : CategoryTheory.MonoidalCategory.tensorObj s.X s.X ⟶ s.X
- one_mul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom s.one (CategoryTheory.CategoryStruct.id s.X)) s.mul = (CategoryTheory.MonoidalCategory.leftUnitor s.X).hom
- mul_one : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id s.X) s.one) s.mul = (CategoryTheory.MonoidalCategory.rightUnitor s.X).hom
- mul_assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom s.mul (CategoryTheory.CategoryStruct.id s.X)) s.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator s.X s.X s.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id s.X) s.mul) s.mul)
- mul_comm : CategoryTheory.CategoryStruct.comp (β_ s.X s.X).hom s.mul = s.mul
A commutative monoid object internal to a monoidal category.
Instances For
The trivial commutative monoid object. We later show this is initial in CommMon_ C
.
Instances For
The forgetful functor from commutative monoid objects to monoid objects.
Instances For
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
.
Instances For
mapCommMon
is functorial in the lax braided functor.
Instances For
Implementation of CommMon_.equivLaxBraidedFunctorPunit
.
Instances For
Implementation of CommMon_.equivLaxBraidedFunctorPunit
.
Instances For
Implementation of CommMon_.equivLaxBraidedFunctorPunit
.
Instances For
Implementation of CommMon_.equivLaxBraidedFunctorPunit
.
Instances For
Commutative monoid objects in C
are "just" braided lax monoidal functors from the trivial
braided monoidal category to C
.