English
If a category C is skeletal and monoidal, its skeleton inherits a monoid structure with multiplication given by the tensor product and unit given by the tensor unit; associativity follows from the associator of C.
Русский
Если категория C скелетна и моноидальна, её скелет наследует структуру моноида с умножением заданным тензорированием и единицей тензорной единицы; ассоциатор задаёт ассоциативность.
LaTeX
$$$\\text{Monoid}(\\mathrm{Skeleton}\\; C)$ with\\ mul(X,Y) = X ⊗ Y, \\\\ one = 1_C, \\\\ mul\\_assoc, mul\\_one, one\\_mul$$$
Lean4
/-- If `C` is monoidal and skeletal, it is a monoid.
See note [reducible non-instances]. -/
abbrev monoidOfSkeletalMonoidal (hC : Skeletal C) : Monoid C
where
mul X Y := (X ⊗ Y : C)
one := (𝟙_ C : C)
one_mul X := hC ⟨λ_ X⟩
mul_one X := hC ⟨ρ_ X⟩
mul_assoc X Y Z := hC ⟨α_ X Y Z⟩
