stabilizer_smul_eq_stabilizer_map_conj

English

There is a canonical isomorphism between stabilizers of two elements in the same orbit, given by conjugation.

Русский

Существуют канонические изоморфизмы стабилизаторов двух элементов одной орбиты, задаваемые конъугацией.

LaTeX

$$stabilizer G a ≃* stabilizer G b$$

Lean4

/-- If the stabilizer of `a` is `S`, then the stabilizer of `g • a` is `gSg⁻¹`. -/
theorem stabilizer_smul_eq_stabilizer_map_conj (g : G) (a : α) :
    stabilizer G (g • a) = (stabilizer G a).map (MulAut.conj g).toMonoidHom :=
  by
  ext h
  rw [mem_stabilizer_iff, ← smul_left_cancel_iff g⁻¹, smul_smul, smul_smul, smul_smul, inv_mul_cancel, one_smul, ←
    mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]

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