Documentation

Mathlib.CategoryTheory.Monoidal.Skeleton

The monoid on the skeleton of a monoidal category #

The skeleton of a monoidal category is a monoid.

Main results #

source
@[reducible, inline]
abbrev 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
Instances For
    source
    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
    Instances For
      source
      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
      source
      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
      source
      theorem CategoryTheory.Skeleton.mul_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X Y : CategoryTheory.Skeleton C) :
      X * Y = CategoryTheory.toSkeleton (CategoryTheory.MonoidalCategoryStruct.tensorObj (Quotient.out X) (Quotient.out Y))
      source
      theorem CategoryTheory.Skeleton.one_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] :
      1 = CategoryTheory.toSkeleton (𝟙_ C)
      source
      theorem CategoryTheory.Skeleton.toSkeleton_tensorObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X Y : C) :
      CategoryTheory.toSkeleton (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) = CategoryTheory.toSkeleton X * CategoryTheory.toSkeleton Y
      source
      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
      source
      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