English
For a pretransitive action, there is a direct equivalence between IsMultiplyPretransitive for the action and IsMultiplyPretransitive for the stabilizer action after applying a construction (ofStabilizer).
Русский
Для предперенитивного действия существует эквивалентность между IsMultiplyPretransitive для самого действия и IsMultiplyPretransitive для связанного со стабилизатором действия после применения соответствующей конструкции (ofStabilizer).
LaTeX
$$$IsMultiplyPretransitive\ G\ α\ (n+1) \iff IsMultiplyPretransitive\ (stabilizer\ G\ a)\ (ofStabilizer\ G\ a)\ n$$$
Lean4
/-- The `fixingSubgroup` of a finite subset of cardinal `d`
in an `n`-transitive action acts `n-d`-transitively on the complement. -/
@[to_additive /-- The `fixingSubgroup` of a finite subset of cardinal `d`
in an `n`-transitive additive action acts `n-d`-transitively on the complement. -/
]
theorem isMultiplyPretransitive {m n : ℕ} [Hn : IsMultiplyPretransitive G α n] (s : Set α) [Finite s]
(hmn : s.ncard + m = n) : IsMultiplyPretransitive (fixingSubgroup G s) (ofFixingSubgroup G s) m where
exists_smul_eq x
y := by
have : IsMultiplyPretransitive G α (s.ncard + m) := by rw [hmn]; infer_instance
have Hs : Nonempty (Fin (s.ncard) ≃ s) := Finite.card_eq.mp (by simp [Nat.card_coe_set_eq])
set x' := ofFixingSubgroup.append x with hx
set y' := ofFixingSubgroup.append y with hy
obtain ⟨g, hg⟩ := exists_smul_eq G x' y'
suffices g ∈ fixingSubgroup G s by
use ⟨g, this⟩
ext i
rw [smul_apply, SetLike.val_smul, Subgroup.mk_smul]
simp [← ofFixingSubgroup.append_right, ← smul_apply, ← hx, ← hy, hg]
intro a
set i := (Classical.choice Hs).symm a
have ha : (Classical.choice Hs) i = a := by simp [i]
rw [← ha]
nth_rewrite 1 [← ofFixingSubgroup.append_left x i]
rw [← ofFixingSubgroup.append_left y i, ← hy, ← hg, smul_apply, ← hx]
