English
A generalization: if hG is IsPreprimitive and we have s with |s|=n+1 and hprim = IsPreprimitive (fixingSubgroup G s), then IsMultiplyPreprimitive G α (n+2).
Русский
Обобщение: если hG IsPreprimitive, и есть s с |s|=n+1, и hprim = IsPreprimitive (fixingSubgroup G s), то IsMultiplyPreprimitive G α (n+2).
LaTeX
$$IsMultiplyPreprimitive G α (n+2)$$
Lean4
/-- Jordan's multiple primitivity criterion (Wielandt, 13.3) -/
theorem isMultiplyPreprimitive (hG : IsPreprimitive G α) {s : Set α} {n : ℕ} (hsn : s.ncard = n + 1)
(hsn' : n + 2 < Nat.card α) (hprim : IsPreprimitive (fixingSubgroup G s) (ofFixingSubgroup G s)) :
IsMultiplyPreprimitive G α (n + 2) :=
by
have hα : Finite α := Or.resolve_right (finite_or_infinite α) (fun _ ↦ by simp [Nat.card_eq_zero_of_infinite] at hsn')
induction n generalizing α hα G with
| zero => -- case n = 0
have : IsPretransitive G α := hG.toIsPretransitive
simp only [zero_add, Set.ncard_eq_one] at hsn
obtain ⟨a, rfl⟩ := hsn
constructor
· rw [ofStabilizer.isMultiplyPretransitive (a := a), is_one_pretransitive_iff]
apply IsPretransitive.of_surjective_map ofFixingSubgroup_of_singleton_bijective.surjective hprim.toIsPretransitive
· intro t h
rw [zero_add, Nat.cast_ofNat, ← one_add_one_eq_two,
(ENat.add_left_injective_of_ne_top ENat.one_ne_top).eq_iff] at h
obtain ⟨b, htb⟩ := Set.encard_eq_one.mp h
obtain ⟨g, hg⟩ := exists_smul_eq G a b
have hst : g • ({ a } : Set α) = ({ b } : Set α) := by rw [Set.smul_set_singleton, hg]
rw [htb]
refine IsPreprimitive.of_surjective (conjMap_ofFixingSubgroup_bijective (hst := hst)).surjective
| succ n
hrec =>
suffices ∃ (a : α) (t : Set (SubMulAction.ofStabilizer G a)), a ∈ s ∧ s = insert a (Subtype.val '' t)
by
obtain ⟨a, t, _, hst⟩ := this
have ha' : a ∉ Subtype.val '' t := by
intro h; rw [Set.mem_image] at h; obtain ⟨x, hx⟩ := h
apply x.prop; rw [hx.right]; exact Set.mem_singleton a
have ht_prim : IsPreprimitive (stabilizer G a) (SubMulAction.ofStabilizer G a) :=
by
rw [← is_one_preprimitive_iff]
rw [← isMultiplyPreprimitive_succ_iff_ofStabilizer]
· apply is_two_preprimitive hG hsn hsn' hprim
· norm_num
have :
IsPreprimitive ↥(fixingSubgroup G (insert a (Subtype.val '' t)))
(ofFixingSubgroup G (insert a (Subtype.val '' t))) :=
IsPreprimitive.of_surjective (ofFixingSubgroup_of_eq_bijective (hst := hst)).surjective
have hGs' : IsPreprimitive (fixingSubgroup (stabilizer G a) t) (ofFixingSubgroup (stabilizer G a) t) :=
IsPreprimitive.of_surjective ofFixingSubgroup_insert_map_bijective.surjective
rw [isMultiplyPreprimitive_succ_iff_ofStabilizer G (a := a) _ (Nat.le_add_left 1 (n + 1))]
refine hrec ht_prim ?_ ?_ hGs' Subtype.finite
· -- t.card = Nat.succ n
rw [← Set.ncard_image_of_injective t Subtype.val_injective]
apply Nat.add_right_cancel
rw [← Set.ncard_insert_of_notMem ha', ← hst, hsn]
· -- n + 2 < Nat.card (SubMulAction.ofStabilizer G α a)
rw [← Nat.add_lt_add_iff_right, nat_card_ofStabilizer_add_one_eq]
exact hsn'
suffices s.Nonempty by
obtain ⟨a, ha⟩ := this
use a, Subtype.val ⁻¹' s, ha
ext x
by_cases hx : x = a <;> simp [hx, mem_ofStabilizer_iff, ha]
rw [← Set.ncard_pos, hsn]; apply Nat.succ_pos
