The monoid on the skeleton of a monoidal category #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The skeleton of a monoidal category is a monoid.
@[reducible]
def
category_theory.monoid_of_skeletal_monoidal
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(hC : category_theory.skeletal C) :
monoid C
If C is monoidal and skeletal, it is a monoid.
See note [reducible non-instances].
Equations
- category_theory.monoid_of_skeletal_monoidal hC = {mul := λ (X Y : C), X ⊗ Y, mul_assoc := _, one := 𝟙_ C _inst_2, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul C), npow_zero' := _, npow_succ' := _}
def
category_theory.comm_monoid_of_skeletal_braided
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
(hC : category_theory.skeletal C) :
If C is braided and skeletal, it is a commutative monoid.
Equations
- category_theory.comm_monoid_of_skeletal_braided hC = {mul := monoid.mul (category_theory.monoid_of_skeletal_monoidal hC), mul_assoc := _, one := monoid.one (category_theory.monoid_of_skeletal_monoidal hC), one_mul := _, mul_one := _, npow := monoid.npow (category_theory.monoid_of_skeletal_monoidal hC), npow_zero' := _, npow_succ' := _, mul_comm := _}
@[protected, instance]
noncomputable
def
category_theory.skeleton.monoidal_category
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C] :
The skeleton of a monoidal category has a monoidal structure itself, induced by the equivalence.
@[protected, instance]
noncomputable
def
category_theory.skeleton.monoid
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category 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
- category_theory.skeleton.monoid = category_theory.monoid_of_skeletal_monoidal category_theory.skeleton.monoid._proof_1