mathlib documentation

category_theory.monoidal.skeleton

The monoid on the skeleton of a monoidal category #

The skeleton of a monoidal category is a monoid.

@[reducible]

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

Equations
@[protected, instance]

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

Equations
@[protected, instance]

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