one_eq_one — Mathlib

English

For a monoid object M, the unit map η equals the canonical unit morphism 1 → M; i.e., the unit morphism is determined by the unit element of M.

Русский

Для моноидального объекта M отображение единицы η равно каноническому морфизму 1 → M; другими словами, единичный морфизм задаётся единицей моноида M.

LaTeX

$$$ \\eta = 1_{M} : \\mathbf{1} \\to M $$$

Lean4

theorem one_eq_one : η = (1 : _ ⟶ M) :=
  show _ = _ ≫ _ by rw [toUnit_unique (toUnit _) (𝟙 _), Category.id_comp]

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