English
For a fixed x ∈ X, the stabilizer submonoid of M at x is canonically isomorphic to the endomorphism monoid of the object x in the action category; this isomorphism is canonical (definitionally equivalent).
Русский
Для фиксированного x ∈ X стабилизатор подмоноида M, действующего на x, канонически изоморфен монойду эндоморфизмов объекта x в категории действия; этот изоморфизм каноничен (определителен).
LaTeX
$$$\operatorname{stabilizerSubmonoid} \, M \, x \cong_* \operatorname{End}_{\mathsf{ActionCategory}(M,X)}(x)$$$
Lean4
/-- The stabilizer of a point is isomorphic to the endomorphism monoid at the
corresponding point. In fact they are definitionally equivalent. -/
def stabilizerIsoEnd : stabilizerSubmonoid M x ≃* @End (ActionCategory M X) _ x :=
MulEquiv.refl _
