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.

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

        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.
        Instances For