Documentation

Mathlib.CategoryTheory.Monoidal.CommMon_

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

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

Instances For
    theorem CommMon_.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A : CommMon_ C} {B : CommMon_ C} (f : A B) (g : A B) (h : f.hom = g.hom) :
    f = g

    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

        Commutative monoid objects in C are "just" braided lax monoidal functors from the trivial braided monoidal category to C.

        Instances For