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].

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev 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.

Equations

• CategoryTheory.commMonoidOfSkeletalBraided hC = { toMonoid := CategoryTheory.monoidOfSkeletalMonoidal hC, mul_comm := ⋯ }

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.

Equations

• CategoryTheory.Skeleton.instMonoidalCategory = CategoryTheory.Monoidal.transport (CategoryTheory.skeletonEquivalence C).symm

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.

Equations

• CategoryTheory.Skeleton.instMonoid = CategoryTheory.monoidOfSkeletalMonoidal ⋯

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.

Equations

• CategoryTheory.Skeleton.instBraidedCategory = CategoryTheory.BraidedCategory.ofFullyFaithful (CategoryTheory.Monoidal.equivalenceTransported (CategoryTheory.skeletonEquivalence C).symm).inverse

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.

Equations

• CategoryTheory.Skeleton.instCommMonoid = CategoryTheory.commMonoidOfSkeletalBraided ⋯

noncomputable instance CategoryTheory.instMonoidalSkeletonFunctorSkeletonEquivalence {C : Type u} [Category.{v, u} C] [MonoidalCategory C] : (skeletonEquivalence C).functor.Monoidal

Equations

• CategoryTheory.instMonoidalSkeletonFunctorSkeletonEquivalence = inferInstanceAs (CategoryTheory.Monoidal.equivalenceTransported (CategoryTheory.skeletonEquivalence C).symm).inverse.Monoidal

noncomputable instance CategoryTheory.instMonoidalSkeletonInverseSkeletonEquivalence {C : Type u} [Category.{v, u} C] [MonoidalCategory C] : (skeletonEquivalence C).inverse.Monoidal

Equations

• CategoryTheory.instMonoidalSkeletonInverseSkeletonEquivalence = inferInstanceAs (CategoryTheory.Monoidal.equivalenceTransported (CategoryTheory.skeletonEquivalence C).symm).functor.Monoidal

noncomputable instance CategoryTheory.instLaxMonoidalSkeletonMapSkeleton {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {D : Type u_1} [Category.{u_2, u_1} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] : F.mapSkeleton.LaxMonoidal

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.instOplaxMonoidalSkeletonMapSkeleton {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {D : Type u_1} [Category.{u_2, u_1} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] : F.mapSkeleton.OplaxMonoidal

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.instMonoidalSkeletonMapSkeleton {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {D : Type u_1} [Category.{u_2, u_1} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] : F.mapSkeleton.Monoidal

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Skeletal.monoidHom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {D : Type u_1} [Category.{u_2, u_1} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (hC : Skeletal C) (hD : Skeletal D) : have x := monoidOfSkeletalMonoidal hC; have x_1 := monoidOfSkeletalMonoidal hD; C →* D

A monoidal functor between skeletal monoidal categories induces a monoid homomorphism.

Equations

• CategoryTheory.Skeletal.monoidHom F hC hD = { toFun := F.obj, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def CategoryTheory.Skeleton.monoidHom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {D : Type u_1} [Category.{u_2, u_1} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] : Skeleton C →* Skeleton D

A monoidal functor between monoidal categories induces a monoid homomorphism between the skeleta.

Equations

• CategoryTheory.Skeleton.monoidHom F = CategoryTheory.Skeletal.monoidHom F.mapSkeleton ⋯ ⋯

def CategoryTheory.Skeletal.mulEquiv {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {D : Type u_1} [Category.{u_2, u_1} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] (hC : Skeletal C) (hD : Skeletal D) : have x := monoidOfSkeletalMonoidal hC; have x_1 := monoidOfSkeletalMonoidal hD; C ≃* D

A monoidal equivalence between skeletal monoidal categories induces a monoid isomorphism.

Equations

• CategoryTheory.Skeletal.mulEquiv e hC hD = { toFun := e.functor.obj, invFun := e.inverse.obj, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

noncomputable def CategoryTheory.Skeleton.mulEquiv {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {D : Type u_1} [Category.{u_2, u_1} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] : Skeleton C ≃* Skeleton D

A monoidal equivalence between monoidal categories induces a monoid isomorphism between the skeleta.

Equations

• CategoryTheory.Skeleton.mulEquiv e = CategoryTheory.Skeletal.mulEquiv (((CategoryTheory.skeletonEquivalence C).trans e).trans (CategoryTheory.skeletonEquivalence D).symm) ⋯ ⋯