The monoid on the skeleton of a monoidal category #
The skeleton of a monoidal category is a monoid.
Main results #
Skeleton.instMonoid
, for monoidal categories.Skeleton.instCommMonoid
, for braided monoidal categories.
If C
is monoidal and skeletal, it is a monoid.
See note [reducible non-instances].
Equations
- CategoryTheory.monoidOfSkeletalMonoidal hC = Monoid.mk ⋯ ⋯ npowRec ⋯ ⋯
Instances For
If C
is braided and skeletal, it is a commutative monoid.
Equations
Instances For
The skeleton of a monoidal category has a monoidal structure itself, induced by the equivalence.
Equations
- CategoryTheory.Skeleton.instMonoidalCategory = CategoryTheory.Monoidal.transport (CategoryTheory.skeletonEquivalence C).symm
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
- CategoryTheory.Skeleton.instMonoid = CategoryTheory.monoidOfSkeletalMonoidal ⋯
The skeleton of a braided monoidal category has a braided monoidal structure itself, induced by the equivalence.
Equations
- CategoryTheory.Skeleton.instBraidedCategory = CategoryTheory.braidedCategoryOfFullyFaithful (CategoryTheory.Monoidal.fromTransported (CategoryTheory.skeletonEquivalence C).symm)
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
- CategoryTheory.Skeleton.instCommMonoid = CategoryTheory.commMonoidOfSkeletalBraided ⋯