English
Let G be IsPreprimitive on α. For a subset s with |s| = n+1 and |α| large, there are two implications: (i) if fixingSubgroup G s acts pretransitively, then IsMultiplyPretransitive G α 2; (ii) if fixingSubgroup G s is preprimitive, then IsMultiplyPreprimitive G α 2.
Русский
Пусть G — IsPreprimitive на α. Для подмножества s с |s| = n+1 и большой размер α существуют две импликации: если fixingSubgroup G s действует пре-транзивно, то IsMultiplyPretransitive G α 2; если fixingSubgroup G s является преprimitive, то IsMultiplyPreprimitive G α 2.
LaTeX
$$IsPretransitive(G_fixing(s)) ⇒ IsMultiplyPretransitive(G, α, 2) and IsPreprimitive(G_fixing(s)) ⇒ IsMultiplyPreprimitive(G, α, 2)$$
Lean4
/-- Simultaneously prove `MulAction.IsPreprimitive.is_two_pretransitive`
and `MulAction.IsPreprimitive.is_two_preprimitive`. -/
theorem is_two_motive_of_is_motive (hG : IsPreprimitive G α) {s : Set α} {n : ℕ} (hsn : s.ncard = n + 1)
(hsn' : n + 2 < Nat.card α) :
(IsPretransitive (fixingSubgroup G s) (ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
(IsPreprimitive (fixingSubgroup G s) (ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2) :=
by
induction n using Nat.strong_induction_on generalizing α G with
| h n
hrec =>
have : Finite α := Or.resolve_right (finite_or_infinite α) (fun _ ↦ by simp [Nat.card_eq_zero_of_infinite] at hsn')
have hs_ne_top : s ≠ ⊤ := by
intro hs
rw [hs, Set.top_eq_univ, Set.ncard_univ] at hsn
simp only [hsn, add_lt_add_iff_left, Nat.not_ofNat_lt_one] at hsn'
have hs_nonempty : s.Nonempty := by
simp [← Set.ncard_pos s.toFinite, hsn]
-- The result is assumed by induction for sets of ncard ≤ n
rcases Nat.lt_or_ge (n + 1) 2 with hn | hn
· -- When n + 1 < 2 (imposes n = 0)
have hn : n = 0 := by rwa [Nat.succ_lt_succ_iff, Nat.lt_one_iff] at hn
simp only [hn, zero_add, Set.ncard_eq_one] at hsn
obtain ⟨a, hsa⟩ := hsn
suffices IsPretransitive (fixingSubgroup G s) (ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
by
refine ⟨this, fun hs_prim ↦ ?_⟩
rw [hsa] at hs_prim
rw [isMultiplyPreprimitive_succ_iff_ofStabilizer G α le_rfl (a := a), is_one_preprimitive_iff]
exact IsPreprimitive.of_surjective ofFixingSubgroup_of_singleton_bijective.surjective
rw [hsa]
rw [ofStabilizer.isMultiplyPretransitive (a := a)]
rw [is_one_pretransitive_iff]
exact IsPretransitive.of_surjective_map ofFixingSubgroup_of_singleton_bijective.surjective
rcases Nat.lt_or_ge (2 * (n + 1)) (Nat.card α) with hn1 | hn2
· -- CASE where 2 * s.ncard < Nat.card α
-- get a, b ∈ s, a ≠ b
have : 1 < s.ncard := by rwa [hsn]
rw [Set.one_lt_ncard] at this
obtain ⟨a, ha, b, hb, hab⟩ := this
obtain ⟨g, hga, hgb⟩ := exists_mem_smul_and_notMem_smul (G := G) s.toFinite hs_nonempty hs_ne_top hab
let t := s ∩ g • s
have ht : t.Finite := s.toFinite.inter_of_left (g • s)
have htm : t.ncard = t.ncard - 1 + 1 :=
by
apply (Nat.sub_eq_iff_eq_add ?_).mp rfl
rw [Nat.one_le_iff_ne_zero]
apply Set.ncard_ne_zero_of_mem (a := a) _ ht
exact ⟨ha, hga⟩
have hmn : t.ncard - 1 < n :=
by
rw [Nat.lt_iff_add_one_le, ← htm, Nat.le_iff_lt_add_one, ← hsn]
apply Set.ncard_lt_ncard _ s.toFinite
exact ⟨Set.inter_subset_left, fun h ↦ hgb (Set.inter_subset_right (h hb))⟩
have htm' : t.ncard - 1 + 2 < Nat.card α := lt_trans (Nat.add_lt_add_right hmn 2) hsn'
suffices IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
by
refine ⟨this, fun hs_prim ↦ ?_⟩
have ht_prim : IsPreprimitive (fixingSubgroup G t) (ofFixingSubgroup G t) :=
by
apply IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter hs_prim
apply Set.union_ne_univ_of_ncard_add_ncard_lt
rwa [Set.ncard_smul_set, hsn, ← two_mul]
apply (hrec (t.ncard - 1) hmn hG htm htm').2 ht_prim
intro hs_trans
have ht_trans : IsPretransitive (fixingSubgroup G t) (ofFixingSubgroup G t) :=
IsPretransitive.isPretransitive_ofFixingSubgroup_inter hs_trans
(by
apply Set.union_ne_univ_of_ncard_add_ncard_lt
rwa [Set.ncard_smul_set, hsn, ← two_mul])
apply (hrec (t.ncard - 1) hmn hG htm ?_).1 ht_trans
apply lt_trans _ hsn'
exact Nat.add_lt_add_right hmn 2
· -- CASE : 2 * s.ncard ≥ Nat.card α
have : Set.Nontrivial sᶜ := by
rwa [← Set.one_lt_encard_iff_nontrivial, ← sᶜ.toFinite.cast_ncard_eq, Nat.one_lt_cast, ←
Nat.add_lt_add_iff_left, Set.ncard_add_ncard_compl, add_comm, hsn, add_comm]
-- get a, b ∈ sᶜ, a ≠ b
obtain ⟨a, ha : a ∈ sᶜ, b, hb : b ∈ sᶜ, hab⟩ := this
obtain ⟨g, hga, hgb⟩ :=
exists_mem_smul_and_notMem_smul (G := G) sᶜ.toFinite (Set.nonempty_of_mem ha)
(by simpa [Set.nonempty_iff_ne_empty] using hs_nonempty) hab
let t := s ∩ g • s
have ha : a ∉ s ∪ g • s := by
simp only [Set.smul_set_compl, Set.mem_compl_iff] at hga ha
simp [ha, hga]
have htm : t.ncard = t.ncard - 1 + 1 :=
by
apply (Nat.sub_eq_iff_eq_add ?_).mp rfl
rw [Nat.one_le_iff_ne_zero, ← Nat.pos_iff_ne_zero, Set.ncard_pos]
apply Set.nonempty_inter_of_le_ncard_add_ncard
· rw [Set.ncard_smul_set, ← two_mul, hsn]; exact hn2
· exact fun h ↦ ha (by rw [h]; trivial)
have hmn : t.ncard - 1 < n :=
by
rw [Nat.lt_iff_add_one_le, ← htm, Nat.le_iff_lt_add_one, ← hsn]
apply Set.ncard_lt_ncard _ (Set.toFinite s)
refine ⟨Set.inter_subset_left, fun h ↦ hb ?_⟩
suffices s = g • s by
rw [this]
simpa only [Set.smul_set_compl, Set.mem_compl_iff, Set.not_notMem] using hgb
apply Set.eq_of_subset_of_ncard_le _ _ (g • s).toFinite
· exact subset_trans h Set.inter_subset_right
· rw [Set.ncard_smul_set]
have htm' : t.ncard - 1 + 2 < Nat.card α := lt_trans (Nat.add_lt_add_right hmn 2) hsn'
have hsgs_ne_top : s ∪ g • s ≠ ⊤ := fun h ↦ ha (h ▸ Set.mem_univ a)
suffices IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
by
refine ⟨this, fun hs_prim ↦ ?_⟩
apply (hrec _ hmn hG htm htm').2
exact IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter hs_prim hsgs_ne_top
intro hs_trans
apply (hrec _ hmn hG htm htm').1
exact IsPretransitive.isPretransitive_ofFixingSubgroup_inter hs_trans hsgs_ne_top
