# mathlibdocumentation

group_theory.sylow

# Sylow theorems #

The Sylow theorems are the following results for every finite group G and every prime number p.

• There exists a Sylow p-subgroup of G.
• All Sylow p-subgroups of G are conjugate to each other.
• Let nₚ be the number of Sylow p-subgroups of G, then nₚ divides the index of the Sylow p-subgroup, nₚ ≡ 1 [MOD p], and nₚ is equal to the index of the normalizer of the Sylow p-subgroup in G.

## Main definitions #

• sylow p G : The type of Sylow p-subgroups of G.

## Main statements #

• exists_subgroup_card_pow_prime: A generalization of Sylow's first theorem: For every prime power pⁿ dividing the cardinality of G, there exists a subgroup of G of order pⁿ.
• is_p_group.exists_le_sylow: A generalization of Sylow's first theorem: Every p-subgroup is contained in a Sylow p-subgroup.
• sylow_conjugate: A generalization of Sylow's second theorem: If the number of Sylow p-subgroups is finite, then all Sylow p-subgroups are conjugate.
• card_sylow_modeq_one: A generalization of Sylow's third theorem: If the number of Sylow p-subgroups is finite, then it is congruent to 1 modulo p.
structure sylow (p : ) (G : Type u_1) [group G] :
Type u_1

A Sylow p-subgroup is a maximal p-subgroup.

@[instance]
def sylow.subgroup.has_coe {p : } {G : Type u_1} [group G] :
Equations
@[simp]
theorem sylow.to_subgroup_eq_coe {p : } {G : Type u_1} [group G] {P : G} :
@[ext]
theorem sylow.ext {p : } {G : Type u_1} [group G] {P Q : G} (h : P = Q) :
P = Q
theorem sylow.ext_iff {p : } {G : Type u_1} [group G] {P Q : G} :
P = Q P = Q
@[instance]
def sylow.set_like {p : } {G : Type u_1} [group G] :
set_like (sylow p G) G
Equations
theorem is_p_group.exists_le_sylow {p : } {G : Type u_1} [group G] {P : subgroup G} (hP : P) :
∃ (Q : G), P Q

A generalization of Sylow's first theorem. Every p-subgroup is contained in a Sylow p-subgroup.

@[instance]
def sylow.nonempty {p : } {G : Type u_1} [group G] :
@[instance]
def sylow.inhabited {p : } {G : Type u_1} [group G] :
Equations
@[instance]
def sylow.pointwise_mul_action {p : } {G : Type u_1} [group G] {α : Type u_2} [group α]  :
(sylow p G)

subgroup.pointwise_mul_action preserves Sylow subgroups.

Equations
theorem sylow.pointwise_smul_def {p : } {G : Type u_1} [group G] {α : Type u_2} [group α] {g : α} {P : G} :
(g P) = g P
@[instance]
def sylow.mul_action {p : } {G : Type u_1} [group G] :
(sylow p G)
Equations
theorem sylow.smul_def {p : } {G : Type u_1} [group G] {g : G} {P : G} :
g P =
theorem sylow.coe_subgroup_smul {p : } {G : Type u_1} [group G] {g : G} {P : G} :
(g P) =
theorem sylow.coe_smul {p : } {G : Type u_1} [group G] {g : G} {P : G} :
(g P) =
theorem sylow.smul_eq_iff_mem_normalizer {p : } {G : Type u_1} [group G] {g : G} {P : G} :
g P = P
theorem subgroup.sylow_mem_fixed_points_iff {p : } {G : Type u_1} [group G] (H : subgroup G) {P : G} :
P (sylow p G)
theorem is_p_group.inf_normalizer_sylow {p : } {G : Type u_1} [group G] {P : subgroup G} (hP : P) (Q : G) :
= P Q
theorem is_p_group.sylow_mem_fixed_points_iff {p : } {G : Type u_1} [group G] {P : subgroup G} (hP : P) {Q : G} :
Q (sylow p G) P Q
@[instance]
def sylow.mul_action.is_pretransitive {p : } {G : Type u_1} [group G] [hp : fact (nat.prime p)] [fintype (sylow p G)] :
(sylow p G)

A generalization of Sylow's second theorem. If the number of Sylow p-subgroups is finite, then all Sylow p-subgroups are conjugate.

theorem card_sylow_modeq_one (p : ) (G : Type u_1) [group G] [fact (nat.prime p)] [fintype (sylow p G)] :

A generalization of Sylow's third theorem. If the number of Sylow p-subgroups is finite, then it is congruent to 1 modulo p.

@[simp]
theorem sylow.orbit_eq_top {p : } {G : Type u_1} [group G] [fact (nat.prime p)] [fintype (sylow p G)] (P : G) :
theorem sylow.stabilizer_eq_normalizer {p : } {G : Type u_1} [group G] (P : G) :
def sylow.equiv_quotient_normalizer {p : } {G : Type u_1} [group G] [fact (nat.prime p)] [fintype (sylow p G)] (P : G) :

Sylow p-subgroups are in bijection with cosets of the normalizer of a Sylow p-subgroup

Equations
@[instance]
def quotient_group.quotient.fintype {p : } {G : Type u_1} [group G] [fact (nat.prime p)] [fintype (sylow p G)] (P : G) :
Equations
theorem card_sylow_eq_card_quotient_normalizer {p : } {G : Type u_1} [group G] [fact (nat.prime p)] [fintype (sylow p G)] (P : G) :
theorem card_sylow_eq_index_normalizer {p : } {G : Type u_1} [group G] [fact (nat.prime p)] [fintype (sylow p G)] (P : G) :
theorem card_sylow_dvd_index {p : } {G : Type u_1} [group G] [fact (nat.prime p)] [fintype (sylow p G)] (P : G) :
theorem sylow.normalizer_sup_eq_top {G : Type u_1} [group G] {p : } [fact (nat.prime p)] {N : subgroup G} [N.normal] [fintype (sylow p N)] (P : N) :

Frattini's Argument

theorem quotient_group.card_preimage_mk {G : Type u} [group G] [fintype G] (s : subgroup G) (t : set ) :
Equations
theorem sylow.card_quotient_normalizer_modeq_card_quotient {G : Type u} [group G] [fintype G] {p n : } [hp : fact (nat.prime p)] {H : subgroup G} (hH : = p ^ n) :

If H is a p-subgroup of G, then the index of H inside its normalizer is congruent mod p to the index of H.

theorem sylow.card_normalizer_modeq_card {G : Type u} [group G] [fintype G] {p n : } [hp : fact (nat.prime p)] {H : subgroup G} (hH : = p ^ n) :
[MOD p ^ (n + 1)]

If H is a subgroup of G of cardinality p ^ n, then the cardinality of the normalizer of H is congruent mod p ^ (n + 1) to the cardinality of G.

theorem sylow.prime_dvd_card_quotient_normalizer {G : Type u} [group G] [fintype G] {p n : } [hp : fact (nat.prime p)] (hdvd : p ^ (n + 1) ) {H : subgroup G} (hH : = p ^ n) :

If H is a p-subgroup but not a Sylow p-subgroup, then p divides the index of H inside its normalizer.

theorem sylow.prime_pow_dvd_card_normalizer {G : Type u} [group G] [fintype G] {p n : } [hp : fact (nat.prime p)] (hdvd : p ^ (n + 1) ) {H : subgroup G} (hH : = p ^ n) :
p ^ (n + 1)

If H is a p-subgroup but not a Sylow p-subgroup of cardinality p ^ n, then p ^ (n + 1) divides the cardinality of the normalizer of H.

theorem sylow.exists_subgroup_card_pow_succ {G : Type u} [group G] [fintype G] {p n : } [hp : fact (nat.prime p)] (hdvd : p ^ (n + 1) ) {H : subgroup G} (hH : = p ^ n) :
∃ (K : subgroup G), = p ^ (n + 1) H K

If H is a subgroup of G of cardinality p ^ n, then H is contained in a subgroup of cardinality p ^ (n + 1) if p ^ (n + 1) divides the cardinality of G

theorem sylow.exists_subgroup_card_pow_prime_le {G : Type u} [group G] [fintype G] (p : ) {n m : } [hp : fact (nat.prime p)] (hdvd : p ^ m ) (H : subgroup G) (hH : = p ^ n) (hnm : n m) :
∃ (K : subgroup G), = p ^ m H K

If H is a subgroup of G of cardinality p ^ n, then H is contained in a subgroup of cardinality p ^ m if n ≤ m and p ^ m divides the cardinality of G

theorem sylow.exists_subgroup_card_pow_prime {G : Type u} [group G] [fintype G] (p : ) {n : } [fact (nat.prime p)] (hdvd : p ^ n ) :
∃ (K : subgroup G), = p ^ n

A generalisation of Sylow's first theorem. If p ^ n divides the cardinality of G, then there is a subgroup of cardinality p ^ n