mathlib documentation

group_theory.sylow

Sylow theorems #

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

Main definitions #

Main statements #

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 : sylow p G} :
@[ext]
theorem sylow.ext {p : } {G : Type u_1} [group G] {P Q : sylow p G} (h : P = Q) :
P = Q
theorem sylow.ext_iff {p : } {G : Type u_1} [group G] {P Q : sylow p 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 : is_p_group p P) :
∃ (Q : sylow p 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 α] [mul_distrib_mul_action α G] :
mul_action α (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 α] [mul_distrib_mul_action α G] {g : α} {P : sylow p G} :
(g P) = g P
@[instance]
def sylow.mul_action {p : } {G : Type u_1} [group G] :
Equations
theorem sylow.smul_def {p : } {G : Type u_1} [group G] {g : G} {P : sylow p G} :
theorem sylow.coe_subgroup_smul {p : } {G : Type u_1} [group G] {g : G} {P : sylow p G} :
theorem sylow.coe_smul {p : } {G : Type u_1} [group G] {g : G} {P : sylow p G} :
theorem sylow.smul_eq_iff_mem_normalizer {p : } {G : Type u_1} [group G] {g : G} {P : sylow p G} :
theorem subgroup.sylow_mem_fixed_points_iff {p : } {G : Type u_1} [group G] (H : subgroup G) {P : sylow p G} :
theorem is_p_group.inf_normalizer_sylow {p : } {G : Type u_1} [group G] {P : subgroup G} (hP : is_p_group p P) (Q : sylow p G) :
theorem is_p_group.sylow_mem_fixed_points_iff {p : } {G : Type u_1} [group G] {P : subgroup G} (hP : is_p_group p P) {Q : sylow p G} :
@[instance]
def sylow.mul_action.is_pretransitive {p : } {G : Type u_1} [group G] [hp : fact (nat.prime p)] [fintype (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 : sylow p G) :
theorem sylow.stabilizer_eq_normalizer {p : } {G : Type u_1} [group G] (P : sylow p G) :

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

Equations
theorem card_sylow_eq_index_normalizer {p : } {G : Type u_1} [group G] [fact (nat.prime p)] [fintype (sylow p G)] (P : sylow p G) :
theorem card_sylow_dvd_index {p : } {G : Type u_1} [group G] [fact (nat.prime p)] [fintype (sylow p G)] (P : sylow 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 : sylow p N) :

Frattini's Argument

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 : fintype.card H = p ^ n) :

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) fintype.card G) {H : subgroup G} (hH : fintype.card H = 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) fintype.card G) {H : subgroup G} (hH : fintype.card H = p ^ n) :

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) fintype.card G) {H : subgroup G} (hH : fintype.card H = p ^ n) :
∃ (K : subgroup G), fintype.card K = 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 fintype.card G) (H : subgroup G) (hH : fintype.card H = p ^ n) (hnm : n m) :
∃ (K : subgroup G), fintype.card K = 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 fintype.card G) :
∃ (K : subgroup G), fintype.card K = 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