English
If g is a cycle in Perm α and lies in G, then the corresponding fixing-subgroup action is pretransitive.
Русский
Если g — цикл в Perm α и лежит в G, то соответствующее действие фиксации предтранситивно.
LaTeX
$$IsPretransitive (fixingSubgroup G (g.supportᶜ)) (SubMulAction.ofFixingSubgroup G (g.supportᶜ))$$
Lean4
/-- A primitive subgroup of `Equiv.Perm α` that contains a swap
is the full permutation group (Jordan). -/
theorem eq_top_of_isPreprimitive_of_isSwap_mem (hG : IsPreprimitive G α) (g : Perm α) (h2g : IsSwap g) (hg : g ∈ G) :
G = ⊤ := by
classical
rcases Nat.lt_or_ge (Nat.card α) 3 with hα3 | hα3
· -- trivial case : Nat.card α ≤ 2
rw [Nat.lt_succ_iff] at hα3
apply Subgroup.eq_top_of_card_eq
simp only [Nat.card_eq_fintype_card]
apply le_antisymm (Fintype.card_subtype_le _)
rw [← Nat.card_eq_fintype_card, Nat.card_perm]
refine le_trans (Nat.factorial_le hα3) ?_
rw [Nat.factorial_two]
have : Nonempty G := One.instNonempty
apply Nat.le_of_dvd Fintype.card_pos
rw [← h2g.orderOf, orderOf_submonoid ⟨g, hg⟩]
exact orderOf_dvd_card
obtain ⟨n, hn⟩ := Nat.exists_eq_add_of_le' hα3
have hsc : Set.ncard ((g.support)ᶜ : Set α) = n + 1 :=
by
apply Nat.add_left_cancel
rw [Set.ncard_add_ncard_compl, Set.ncard_coe_finset, card_support_eq_two.mpr h2g, add_comm, hn]
apply eq_top_of_isMultiplyPretransitive
suffices IsMultiplyPreprimitive G α (Nat.card α - 1) by apply IsMultiplyPreprimitive.isMultiplyPretransitive
rw [show Nat.card α - 1 = n + 2 by grind]
apply hG.isMultiplyPreprimitive hsc
· rw [hn]; apply Nat.lt_add_one
have := isPretransitive_of_isCycle_mem h2g.isCycle hg
apply IsPreprimitive.of_prime_card
convert Nat.prime_two
rw [Nat.card_eq_fintype_card, Fintype.card_subtype, ← card_support_eq_two.mpr h2g]
simp [SubMulAction.mem_ofFixingSubgroup_iff, support]
