English
Assume G acts on α and IsPretransitive G α. Then for any a ∈ α, IsMultiplyPretransitive G α (n+1) is equivalent to IsMultiplyPretransitive (stabilizer G a) (ofStabilizer G a) n.
Русский
Пусть G действует на α и выполняется IsPretransitive G α. Тогда для любого a ∈ α выполняется эквивалентность: IsMultiplyPretransitive G α (n+1) эквивалентно IsMultiplyPretransitive (stabilizer G a) (ofStabilizer G a) n.
LaTeX
$$$IsMultiplyPretransitive\, G\ α\ (n+1) \iff IsMultiplyPretransitive\, (stabilizer\ G\ a)\ (ofStabilizer\ G\ a)\ n$$$
Lean4
/-- Multiple transitivity of a pretransitive action
is equivalent to one less transitivity of stabilizer of a point
(Wielandt, th. 9.1, 1st part) -/
@[to_additive /-- Multiple transitivity of a pretransitive action
is equivalent to one less transitivity of stabilizer of a point
[Wielandt, th. 9.1, 1st part][Wielandt-1964]. -/
]
theorem isMultiplyPretransitive [IsPretransitive G α] {n : ℕ} {a : α} :
IsMultiplyPretransitive G α n.succ ↔ IsMultiplyPretransitive (stabilizer G a) (SubMulAction.ofStabilizer G a) n :=
by
refine ⟨fun hn ↦ ⟨fun x y ↦ ?_⟩, fun hn ↦ ⟨fun x y ↦ ?_⟩⟩
· obtain ⟨g, hgxy⟩ := exists_smul_eq G (ofStabilizer.snoc x) (ofStabilizer.snoc y)
have hg : g ∈ stabilizer G a := by
rw [mem_stabilizer_iff]
rw [DFunLike.ext_iff] at hgxy
convert hgxy (last n) <;> simp [smul_apply, ofStabilizer.snoc_last]
use ⟨g, hg⟩
ext i
simp only [smul_apply, SubMulAction.val_smul_of_tower, subgroup_smul_def]
rw [← ofStabilizer.snoc_castSucc x, ← smul_apply, hgxy, ofStabilizer.snoc_castSucc]
· -- gx • x = x1 :: a
obtain ⟨gx, x1, hgx⟩ := exists_smul_of_last_eq G a x
obtain ⟨gy, y1, hgy⟩ := exists_smul_of_last_eq G a y
obtain ⟨g, hg⟩ := hn.exists_smul_eq x1 y1
use gy⁻¹ * g * gx
ext i
simp only [mul_smul, smul_apply, inv_smul_eq_iff]
simp only [← smul_apply _ _ i, hgy, hgx]
simp only [smul_apply]
rcases Fin.eq_castSucc_or_eq_last i with ⟨i, rfl⟩ | ⟨rfl⟩
· simp [ofStabilizer.snoc_castSucc, ← hg, SetLike.val_smul, subgroup_smul_def]
· simp only [ofStabilizer.snoc_last, ← hg]
exact g.prop
