English
For α with card 4, the two-Sylow subgroup image equals the union of {1} and cycleType {2,2} elements inside Alt α.
Русский
При |α| = 4 образ подгруппы Sylow 2 равен объединению {1} и элементов с cycleType {2,2} внутри Alt α.
LaTeX
$$$\text{(Sylow 2-subgroup image)} = \{1\} \cup \{ g\in Alt(α) : (g:Perm α).cycleType = {2,2} \}$$$
Lean4
theorem coe_two_sylow_of_card_eq_four (hα4 : Nat.card α = 4) (S : Sylow 2 (alternatingGroup α)) :
(S : Set (alternatingGroup α)) = { 1 } ∪ {g : alternatingGroup α | (g : Perm α).cycleType = { 2, 2 }} := by
classical
refine Set.eq_of_subset_of_card_le (fun k hk ↦ ?_) ?_
· -- inclusion S ⊆ {1} ∪ {g | cycleType g = { 2, 2 }}
obtain ⟨n, hn⟩ := (IsPGroup.iff_orderOf.mp S.isPGroup') ⟨k, hk⟩
replace hn : (orderOf (k : Perm α)) = 2 ^ n := by simpa using hn
convert mem_kleinFour_of_order_two_pow hα4 k.2 hn.dvd
simp
· -- card (kleinFour α) ≤ card S
simp_rw [← Nat.card_eq_fintype_card]
refine (card_two_sylow_of_card_eq_four hα4 S).symm.trans_ge ?_
rw [Nat.card_eq_card_toFinset, Set.toFinset_union, Set.toFinset_singleton, Set.toFinset_setOf]
apply (Finset.card_union_le _ _).trans
rw [Finset.card_singleton, AlternatingGroup.card_of_cycleType, ← Nat.card_eq_fintype_card, hα4]
decide
