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.

@[reducible, inline]

abbrev CategoryTheory.monoidOfSkeletalMonoidal {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (hC : Skeletal C) : Monoid C

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

def CategoryTheory.commMonoidOfSkeletalBraided {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] (hC : Skeletal C) : CommMonoid C

If C is braided and skeletal, it is a commutative monoid.

noncomputable instance CategoryTheory.Skeleton.instMonoidalCategory {C : Type u} [Category.{v, u} C] [MonoidalCategory C] : MonoidalCategory (Skeleton C)

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

noncomputable instance CategoryTheory.Skeleton.instMonoid {C : Type u} [Category.{v, u} C] [MonoidalCategory C] : Monoid (Skeleton C)

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.

theorem CategoryTheory.Skeleton.mul_eq {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (X Y : Skeleton C) : X * Y = toSkeleton (MonoidalCategoryStruct.tensorObj (Quotient.out X) (Quotient.out Y))

theorem CategoryTheory.Skeleton.one_eq {C : Type u} [Category.{v, u} C] [MonoidalCategory C] : 1 = toSkeleton (MonoidalCategoryStruct.tensorUnit C)

theorem CategoryTheory.Skeleton.toSkeleton_tensorObj {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (X Y : C) : toSkeleton (MonoidalCategoryStruct.tensorObj X Y) = toSkeleton X * toSkeleton Y

noncomputable instance CategoryTheory.Skeleton.instBraidedCategory {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] : BraidedCategory (Skeleton C)

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

noncomputable instance CategoryTheory.Skeleton.instCommMonoid {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] : CommMonoid (Skeleton C)

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.