English
If G is a primitive subgroup of Equiv.Perm α and contains a 3-cycle g, then it contains the alternating group α.
Русский
Если G — примитивная подгруппа Equiv.Perm α и содержит 3-цикл g, то она содержит алтернированную группу α.
LaTeX
$$alternatingGroup α ≤ G$$
Lean4
/-- A primitive subgroup of `Equiv.Perm α` that contains a 3-cycle
contains the alternating group (Jordan). -/
theorem alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem (hG : IsPreprimitive G α) {g : Perm α}
(h3g : IsThreeCycle g) (hg : g ∈ G) : alternatingGroup α ≤ G := by
classical
rcases Nat.lt_or_ge (Nat.card α) 4 with hα4 | hα4
· -- trivial case : Fintype.card α ≤ 3
rw [Nat.lt_succ_iff] at hα4
apply alternatingGroup_le_of_index_le_two
rw [← Nat.mul_le_mul_right_iff (k := Nat.card G) (Nat.card_pos), Subgroup.index_mul_card, Nat.card_perm]
apply le_trans (Nat.factorial_le hα4)
rw [show Nat.factorial 3 = 2 * 3 by simp [Nat.factorial]]
simp only [mul_le_mul_iff_right₀, Nat.succ_pos]
apply Nat.le_of_dvd Nat.card_pos
suffices 3 = orderOf (⟨g, hg⟩ : G) by
rw [this, Nat.card_eq_fintype_card]
exact orderOf_dvd_card
simp only [orderOf_mk, h3g.orderOf]
-- important case : Nat.card α ≥ 4
obtain ⟨n, hn⟩ := Nat.exists_eq_add_of_le' hα4
apply IsMultiplyPretransitive.alternatingGroup_le
suffices IsMultiplyPreprimitive G α (Nat.card α - 2) by apply IsMultiplyPreprimitive.isMultiplyPretransitive
rw [show Nat.card α - 2 = n + 2 by grind]
apply hG.isMultiplyPreprimitive (s := (g.supportᶜ : Set α))
· apply Nat.add_left_cancel
rw [Set.ncard_add_ncard_compl, Set.ncard_coe_finset, h3g.card_support, add_comm, hn]
· grind
have := isPretransitive_of_isCycle_mem h3g.isCycle hg
apply IsPreprimitive.of_prime_card
convert Nat.prime_three
rw [Nat.card_eq_fintype_card, Fintype.card_subtype, ← h3g.card_support]
apply congr_arg
ext x
simp [SubMulAction.mem_ofFixingSubgroup_iff]
