stabilizerEquivStabilizer — Mathlib

English

If b = g • a and x ∈ stabilizer G a, then the image of x under stabilizerEquivStabilizer is MulAut.conj g x.

Русский

Если b = g • a и x ∈ стабилизатор G a, то образ x под stabilizerEquivStabilizer равен MulAut.conj g x.

LaTeX

$$stabilizerEquivStabilizer hg x = MulAut.conj g 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 :=
  ((MulAut.conj g).subgroupMap (stabilizer G a)).trans
    (MulEquiv.subgroupCongr (by rw [hg, stabilizer_smul_eq_stabilizer_map_conj g a, ← MulEquiv.toMonoidHom_eq_coe]))

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