stabilizerEquivStabilizer — Mathlib

English

For hg: b = g + a, and x ∈ stabilizer(a), the image of x under the stabilizer equivalence is given by conjugation by g.

Русский

При $b = g + a$ и $x \\in \\mathrm{stabilizer}(a)$ образ $x$ по эквивелентности стабилизатора задаётся конъюгацией на $g$.

LaTeX

$$$\\text{stabilizerEquivStabilizer } hg\\; x = (\\mathrm{AddAut.conj } g).\\mathrmtoMul x.$$$

Lean4

/-- The natural group equivalence between the stabilizers of two elements in the same orbit. -/
def stabilizerEquivStabilizer (hg : b = g +ᵥ a) : stabilizer G a ≃+ stabilizer G b :=
  AddEquiv.trans ((AddAut.conj g).toMul.addSubgroupMap _)
    (AddEquiv.addSubgroupCongr
      (by rw [hg, stabilizer_vadd_eq_stabilizer_map_conj g a, ← AddEquiv.toAddMonoidHom_eq_coe]))

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