instCommComonObjUnit — Mathlib

English

In a braided monoidal category, the unit object equipped with its canonical comonoid structure forms a commutative comonoid object.

Русский

В браидированной моноидальной категории единичный объект, вооружённый своей канонической структурой комоноида, образует коммутативный комоноид.

LaTeX

$$$\\text{IsCommComon}(\\mathbb{1}_C)$$$

Lean4

/-- The trivial comonoid on the unit object is commutative. -/
instance instCommComonObjUnit : IsCommComonObj (𝟙_ C) where comul_comm := by simp [← unitors_equal]

Похожие утверждения