Documentation

TauCeti.GroupTheory.Perm.SylowFive

Sylow 5-subgroups of S₅ and the orders of its transitive subgroups #

Let α be a type with five elements, so that Equiv.Perm α is the symmetric group S₅ of order 120. Its Sylow 5-subgroups have order 5; there are six of them, and each has a normalizer of order 20.

The main result is a dichotomy for a subgroup G of S₅ whose order is divisible by 5: either G lies between a Sylow 5-subgroup P of S₅ and its normalizer, or G contains the alternating group. The two cases are distinguished by whether G has one or six Sylow 5-subgroups.

Applied to a transitive subgroup, whose order is divisible by 5, this shows that the order of a transitive subgroup of S₅ is one of 5, 10, 20, 60, 120. This is the first half of the classification of the transitive subgroups of S₅: the transitive subgroups of order 60 and 120 are A₅ and S₅, and those of order dividing 20 sit inside the normalizer of a Sylow 5-subgroup.

Main results #

References #

source
theorem TauCeti.sylowFiveFactPrimeFive :
Fact (Nat.Prime 5)
source
theorem TauCeti.card_sylow_five_perm {α : Type u_1} (hα : Nat.card α = 5) :
Nat.card (Sylow 5 (Equiv.Perm α)) = 6

The symmetric group on five points has exactly six Sylow 5-subgroups.

source
theorem TauCeti.card_normalizer_sylow_five_perm {α : Type u_1} (hα : Nat.card α = 5) (P : Sylow 5 (Equiv.Perm α)) :
Nat.card ↥(Subgroup.normalizer ↑P) = 20

The normalizer of a Sylow 5-subgroup of the symmetric group on five points has order 20.

source
theorem TauCeti.card_sylow_five_eq_one_or_six {α : Type u_1} (hα : Nat.card α = 5) (G : Subgroup (Equiv.Perm α)) :
Nat.card (Sylow 5 ↥G) = 1 ∨ Nat.card (Sylow 5 ↥G) = 6

A subgroup of the symmetric group on five points has one or six Sylow 5-subgroups.

source
theorem TauCeti.exists_sylow_le_le_normalizer_of_card_sylow_five_eq_one {α : Type u_1} (hα : Nat.card α = 5) (G : Subgroup (Equiv.Perm α)) (h5 : 5 ∣ Nat.card ↥G) (h1 : Nat.card (Sylow 5 ↥G) = 1) :
∃ (P : Sylow 5 (Equiv.Perm α)), ↑P ≤ G ∧ G ≤ Subgroup.normalizer ↑P

A subgroup G of the symmetric group on five points whose order is divisible by 5 and which has a unique Sylow 5-subgroup lies between a Sylow 5-subgroup of the symmetric group and its normalizer.

source
theorem TauCeti.eq_alternatingGroup_or_eq_top_of_thirty_dvd_natCard {α : Type u_1} (hα : Nat.card α = 5) (G : Subgroup (Equiv.Perm α)) (h30 : 30 ∣ Nat.card ↥G) :
have x := ⋯; have x := Fintype.ofFinite α; have x_1 := Classical.decEq α; G = alternatingGroup α ∨ G = ⊤

A subgroup of the symmetric group on five points whose order is divisible by 30 is the alternating group or the whole symmetric group.

source
theorem TauCeti.exists_sylow_le_le_normalizer_or_alternatingGroup_le {α : Type u_1} (hα : Nat.card α = 5) (G : Subgroup (Equiv.Perm α)) (h5 : 5 ∣ Nat.card ↥G) :
have x := ⋯; have x := Fintype.ofFinite α; have x_1 := Classical.decEq α; (∃ (P : Sylow 5 (Equiv.Perm α)), ↑P ≤ G ∧ G ≤ Subgroup.normalizer ↑P) ∨ alternatingGroup α ≤ G

A subgroup G of the symmetric group on five points whose order is divisible by 5 either lies between a Sylow 5-subgroup of the symmetric group and its normalizer, or contains the alternating group.

source
theorem TauCeti.natCard_mem_of_five_dvd_natCard {α : Type u_1} (hα : Nat.card α = 5) (G : Subgroup (Equiv.Perm α)) (h5 : 5 ∣ Nat.card ↥G) :
Nat.card ↥G ∈ {5, 10, 20, 60, 120}

A subgroup of the symmetric group on five points whose order is divisible by 5 has order 5, 10, 20, 60 or 120.

source
theorem TauCeti.natCard_mem_of_natCard_eq_five_of_isPretransitive {α : Type u_1} (hα : Nat.card α = 5) (G : Subgroup (Equiv.Perm α)) [MulAction.IsPretransitive (↥G) α] :
Nat.card ↥G ∈ {5, 10, 20, 60, 120}

A transitive subgroup of the symmetric group on five points has order 5, 10, 20, 60 or 120.