stabilizer_vadd_eq_stabilizer_map_conj

English

If the stabilizer of x is S, then the stabilizer of g + x is the image of S under conjugation by g (viewed as a group automorphism).

Русский

Если стабилизатор $x$ равен $S$, то стабилизатор $g+x$ равен образу $S$ под конъюгацию на $g$.

LaTeX

$$$\\mathrm{stabilizer}_G(g + x) = \\mathrm{map}_{(\\mathrm{AddAut\\,.conj}\n g)}(\\mathrm{stabilizer}_G(x)).$$$

Lean4

/-- If the stabilizer of `x` is `S`, then the stabilizer of `g +ᵥ x` is `g + S + (-g)`. -/
theorem stabilizer_vadd_eq_stabilizer_map_conj (g : G) (a : α) :
    stabilizer G (g +ᵥ a) = (stabilizer G a).map (AddAut.conj g).toMul.toAddMonoidHom :=
  by
  ext h
  rw [mem_stabilizer_iff, ← vadd_left_cancel_iff (-g), vadd_vadd, vadd_vadd, vadd_vadd, neg_add_cancel, zero_vadd, ←
    mem_stabilizer_iff, AddSubgroup.mem_map_equiv, AddAut.conj_symm_apply]

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