endMulEquivSubgroup — Mathlib

English

For a subgroup H of G, the endomorphism monoid of the object objEquiv G (G ⧸ H) at the unit is canonically isomorphic to H via a specified monoid equivalence.

Русский

Для подгруппы H подмножество концевых моном в объекте objEquiv G (G ⧸ H) у единицы изоморфно подгруппе H посредством заданного изоморфизма моноидов.

LaTeX

$$$\operatorname{End}(\mathrm{objEquiv}(G,(G/H) )\uparrow(1)) \cong_* H$$$

Lean4

/-- Any subgroup of `G` is a vertex group in its action groupoid. -/
def endMulEquivSubgroup (H : Subgroup G) : End (objEquiv G (G ⧸ H) ↑(1 : G)) ≃* H :=
  MulEquiv.trans (stabilizerIsoEnd G ((1 : G) : G ⧸ H)).symm (MulEquiv.subgroupCongr <| stabilizer_quotient H)

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