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]

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

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

Equations

• CategoryTheory.monoidOfSkeletalMonoidal hC = Monoid.mk (_ : ∀ (X : C), 1 * X = X) (_ : ∀ (X : C), X * 1 = X) npowRec

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

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

Equations

• CategoryTheory.commMonoidOfSkeletalBraided hC = let src := CategoryTheory.monoidOfSkeletalMonoidal hC; CommMonoid.mk (_ : ∀ (X Y : C), X * Y = Y * X)

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

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

noncomputable instance CategoryTheory.Skeleton.instMonoid {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : Monoid (CategoryTheory.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.

Equations

• CategoryTheory.Skeleton.instMonoid = CategoryTheory.monoidOfSkeletalMonoidal (_ : CategoryTheory.Skeletal (CategoryTheory.Skeleton C))

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

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)

noncomputable instance CategoryTheory.Skeleton.instCommMonoid {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CommMonoid (CategoryTheory.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.

Equations

• CategoryTheory.Skeleton.instCommMonoid = CategoryTheory.commMonoidOfSkeletalBraided (_ : CategoryTheory.Skeletal (CategoryTheory.Skeleton C))