English
For a normal subgroup N, the orbit of a under N is invariant up to the action: g • orbit N a = orbit N (g • a).
Русский
Для нормальной подгруппы N орбита a под N остается тождественно равной орбите g • a под N: g • orbit_N(a) = orbit_N(g • a).
LaTeX
$$$g \\cdot \\operatorname{orbit}_N(a) = \\operatorname{orbit}_N(g\\cdot a)$$$
Lean4
@[to_additive]
theorem smul_orbit_eq_orbit_smul (N : Subgroup G) [nN : N.Normal] (a : X) (g : G) : g • orbit N a = orbit N (g • a) :=
by
simp only [orbit, Set.smul_set_range]
ext
simp only [Set.mem_range]
constructor
· rintro ⟨⟨k, hk⟩, rfl⟩
use ⟨g * k * g⁻¹, nN.conj_mem k hk g⟩
simp only [Subgroup.mk_smul]
rw [smul_smul, inv_mul_cancel_right, ← smul_smul]
· rintro ⟨⟨k, hk⟩, rfl⟩
use ⟨g⁻¹ * k * g, nN.conj_mem' k hk g⟩
simp only [Subgroup.mk_smul]
simp only [← smul_smul, smul_inv_smul]
