toEnd — Mathlib

English

For a monoid M, the endomorphism monoid of the distinguished object in the single-object category is canonically isomorphic to M.

Русский

Для моноида M концевый моноидEnd(Star) категории с одним объектом из M естественно изоморфен самому M.

LaTeX

$$$M \\cong_* \\mathrm{End}(\\mathrm{SingleObj}.\\mathrm{star}\,M)$$$

Lean4

/-- The endomorphisms monoid of the only object in `SingleObj M` is equivalent to the original
monoid `M`. -/
def toEnd : M ≃* End (SingleObj.star M) :=
  { Equiv.refl M with map_mul' := fun _ _ => rfl }

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