English
The alternating group on α is (|α|−2)-pretransitive.
Русский
Через чередующуюся группу на α обладает (|α|−2)-предтранситивностью.
LaTeX
$$IsMultiplyPretransitive (alternatingGroup α) α (|α| − 2)$$
Lean4
/-- The `alternatingGroup` on α is (card α - 2)-pretransitive. -/
theorem isMultiplyPretransitive : IsMultiplyPretransitive (alternatingGroup α) α (Nat.card α - 2) :=
by
rcases lt_or_ge (Nat.card α) 2 with h2 | h2
· rw [Nat.sub_eq_zero_of_le (le_of_lt h2)]
apply is_zero_pretransitive
have h2le : Nat.card α - 2 ≤ Nat.card α := sub_le (Nat.card α) 2
have := Equiv.Perm.isMultiplyPretransitive α (Nat.card α)
have : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2) :=
MulAction.isMultiplyPretransitive_of_le h2le le_rfl
refine ⟨fun x y ↦ ?_⟩
obtain ⟨g, hg⟩ := exists_smul_eq (Equiv.Perm α) x y
rcases Int.units_eq_one_or (Equiv.Perm.sign g) with h | h
· exact ⟨⟨g, h⟩, hg⟩
· have : (Finset.univ.image x)ᶜ.card = 2 := by
rw [Finset.card_compl, Finset.univ.card_image_of_injective (by exact x.2), Finset.card_univ, ←
Nat.card_eq_fintype_card, Fintype.card_fin, tsub_tsub_cancel_of_le h2]
obtain ⟨a, b, hab, hs⟩ := Finset.card_eq_two.mp this
refine ⟨⟨g * Equiv.swap a b, by simp [h, hab]⟩, ?_⟩
ext i
have h : x i ∈ Finset.univ.image x := Finset.mem_image.mpr ⟨i, Finset.mem_univ i, rfl⟩
rw [← Finset.notMem_compl, hs, Finset.mem_insert, Finset.mem_singleton, not_or] at h
simp [Equiv.swap_apply_of_ne_of_ne h.1 h.2, ← hg]
