The category of commutative monoids in a braided monoidal category. #
A commutative monoid object internal to a monoidal category.
- X : C
- mul_assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.mul self.X) self.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator self.X self.X self.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft self.X self.mul) self.mul)
Instances For
The trivial commutative monoid object. We later show this is initial in CommMon_ C
.
Equations
- CommMon_.trivial C = { toMon_ := Mon_.trivial C, mul_comm := ⋯ }
Instances For
The forgetful functor from commutative monoid objects to monoid objects.
Instances For
The forgetful functor from commutative monoid objects to monoid objects is fully faithful.
Equations
Instances For
Constructor for isomorphisms in the category CommMon_ C
.
Equations
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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
mapCommMon
is functorial in the lax braided functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Implementation of CommMon_.equivLaxBraidedFunctorPUnit
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Implementation of CommMon_.equivLaxBraidedFunctorPUnit
.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Implementation of CommMon_.equivLaxBraidedFunctorPUnit
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Implementation of CommMon_.equivLaxBraidedFunctorPUnit
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Implementation of CommMon_.equivLaxBraidedFunctorPUnit
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Commutative monoid objects in C
are "just" braided lax monoidal functors from the trivial
braided monoidal category to C
.
Equations
- One or more equations did not get rendered due to their size.