English
Units in M map to automorphisms of the star object in the single-object category, forming an isomorphism between Units(M) and Aut(SingleObj.star M).
Русский
Единицы M соответствуют автоматоморфизмам звезды в однообъектной категории, образуя изоморфизм Units(M) ≅ Aut(SingleObj.star M).
LaTeX
$$$\\text{toAut}: M^{\\times} \\cong_* \\mathrm{Aut}(\\mathrm{SingleObj.star}\\,M)$$$
Lean4
/-- The units in a monoid are (multiplicatively) equivalent to
the automorphisms of `star` when we think of the monoid as a single-object category. -/
def toAut : Mˣ ≃* Aut (SingleObj.star M) :=
MulEquiv.trans (Units.mapEquiv (SingleObj.toEnd M)) (Aut.unitsEndEquivAut (SingleObj.star M))
