Documentation

Mathlib.CategoryTheory.Monoidal.Skeleton

The monoid on the skeleton of a monoidal category #

The skeleton of a monoidal category is a monoid.

Main results #

@[reducible, inline]

If C is monoidal and skeletal, it is a monoid. See note [reducible non-instances].

Equations
Instances For

    The skeleton of a monoidal category has a monoidal structure itself, induced by the equivalence.

    Equations

    The skeleton of a monoidal category can be viewed as a monoid, where the multiplication is given by the tensor product, and satisfies the monoid axioms since it is a skeleton.

    Equations

    The skeleton of a braided monoidal category has a braided monoidal structure itself, induced by the equivalence.

    Equations

    The skeleton of a braided monoidal category can be viewed as a commutative monoid, where the multiplication is given by the tensor product, and satisfies the monoid axioms since it is a skeleton.

    Equations