# mathlib3documentation

group_theory.sylow

# Sylow theorems #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.card_eq_multiplicity: The cardinality of a Sylow subgroup is p ^ n where n is the multiplicity of p in the group order.
• 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.

Instances for sylow
@[protected, 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
@[protected, instance]
def sylow.set_like {p : } {G : Type u_1} [group G] :
set_like (sylow p G) G
Equations
@[protected, instance]
def sylow.subgroup_class {p : } {G : Type u_1} [group G] :
@[protected, instance]
def sylow.mul_action_left {p : } {G : Type u_1} [group G] (P : G) {α : Type u_2} [ α] :
α

The action by a Sylow subgroup is the action by the underlying group.

Equations
def sylow.comap_of_ker_is_p_group {p : } {G : Type u_1} [group G] (P : G) {K : Type u_2} [group K] (ϕ : K →* G) (hϕ : (ϕ.ker)) (h : P ϕ.range) :
K

The preimage of a Sylow subgroup under a p-group-kernel homomorphism is a Sylow subgroup.

Equations
@[simp]
theorem sylow.coe_comap_of_ker_is_p_group {p : } {G : Type u_1} [group G] (P : G) {K : Type u_2} [group K] (ϕ : K →* G) (hϕ : (ϕ.ker)) (h : P ϕ.range) :
h) =
def sylow.comap_of_injective {p : } {G : Type u_1} [group G] (P : G) {K : Type u_2} [group K] (ϕ : K →* G) (hϕ : function.injective ϕ) (h : P ϕ.range) :
K

The preimage of a Sylow subgroup under an injective homomorphism is a Sylow subgroup.

Equations
• h = h
@[simp]
theorem sylow.coe_comap_of_injective {p : } {G : Type u_1} [group G] (P : G) {K : Type u_2} [group K] (ϕ : K →* G) (hϕ : function.injective ϕ) (h : P ϕ.range) :
h) =
@[protected]
def sylow.subtype {p : } {G : Type u_1} [group G] (P : G) {N : subgroup G} (h : P N) :
N

A sylow subgroup of G is also a sylow subgroup of a subgroup of G.

Equations
• P.subtype h = sylow.subtype._proof_1 _
@[simp]
theorem sylow.coe_subtype {p : } {G : Type u_1} [group G] (P : G) {N : subgroup G} (h : P N) :
theorem sylow.subtype_injective {p : } {G : Type u_1} [group G] {N : subgroup G} {P Q : G} {hP : P N} {hQ : Q N} (h : P.subtype hP = Q.subtype hQ) :
P = Q
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.

@[protected, instance]
def sylow.nonempty {p : } {G : Type u_1} [group G] :
@[protected, instance]
noncomputable def sylow.inhabited {p : } {G : Type u_1} [group G] :
Equations
theorem sylow.exists_comap_eq_of_ker_is_p_group {p : } {G : Type u_1} [group G] {H : Type u_2} [group H] (P : H) {f : H →* G} (hf : (f.ker)) :
(Q : G), = P
theorem sylow.exists_comap_eq_of_injective {p : } {G : Type u_1} [group G] {H : Type u_2} [group H] (P : H) {f : H →* G} (hf : function.injective f) :
(Q : G), = P
theorem sylow.exists_comap_subtype_eq {p : } {G : Type u_1} [group G] {H : subgroup G} (P : H) :
(Q : G), = P
noncomputable def sylow.fintype_of_ker_is_p_group {p : } {G : Type u_1} [group G] {H : Type u_2} [group H] {f : H →* G} (hf : (f.ker)) [fintype (sylow p G)] :

If the kernel of f : H →* G is a p-group, then fintype (sylow p G) implies fintype (sylow p H).

Equations
noncomputable def sylow.fintype_of_injective {p : } {G : Type u_1} [group G] {H : Type u_2} [group H] {f : H →* G} (hf : function.injective f) [fintype (sylow p G)] :

If f : H →* G is injective, then fintype (sylow p G) implies fintype (sylow p H).

Equations
@[protected, instance]
noncomputable def sylow.fintype {p : } {G : Type u_1} [group G] (H : subgroup G) [fintype (sylow p G)] :

If H is a subgroup of G, then fintype (sylow p G) implies fintype (sylow p H).

Equations
@[protected, instance]
def sylow.finite {p : } {G : Type u_1} [group G] (H : subgroup G) [finite (sylow p G)] :

If H is a subgroup of G, then finite (sylow p G) implies finite (sylow p H).

@[protected, 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
@[protected, 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_le {p : } {G : Type u_1} [group G] {P : G} {H : subgroup G} (hP : P H) (h : H) :
(h P) H
theorem sylow.smul_subtype {p : } {G : Type u_1} [group G] {P : G} {H : subgroup G} (hP : P H) (h : H) :
h P.subtype hP = (h P).subtype _
theorem sylow.smul_eq_iff_mem_normalizer {p : } {G : Type u_1} [group G] {g : G} {P : G} :
theorem sylow.smul_eq_of_normal {p : } {G : Type u_1} [group G] {g : G} {P : G} [h : P.normal] :
g P = P
theorem subgroup.sylow_mem_fixed_points_iff {p : } {G : Type u_1} [group G] (H : subgroup G) {P : G} :
theorem is_p_group.inf_normalizer_sylow {p : } {G : Type u_1} [group G] {P : subgroup G} (hP : P) (Q : G) :
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
@[protected, instance]
def sylow.mul_action.is_pretransitive {p : } {G : Type u_1} [group G] [hp : fact (nat.prime p)] [finite (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.

theorem not_dvd_card_sylow (p : ) (G : Type u_1) [group G] [hp : fact (nat.prime p)] [fintype (sylow p G)] :
def sylow.equiv_smul {p : } {G : Type u_1} [group G] (P : G) (g : G) :
P ≃* (g P)

Sylow subgroups are isomorphic

Equations
noncomputable def sylow.equiv {p : } {G : Type u_1} [group G] [fact (nat.prime p)] [finite (sylow p G)] (P Q : G) :

Sylow subgroups are isomorphic

Equations
@[simp]
theorem sylow.orbit_eq_top {p : } {G : Type u_1} [group G] [fact (nat.prime p)] [finite (sylow p G)] (P : G) :
theorem sylow.stabilizer_eq_normalizer {p : } {G : Type u_1} [group G] (P : G) :
theorem sylow.conj_eq_normalizer_conj_of_mem_centralizer {p : } {G : Type u_1} [group G] [fact (nat.prime p)] [finite (sylow p G)] (P : G) (x g : G) (hx : x ) (hy : g⁻¹ * x * g ) :
(n : G) (H : n P.normalizer), g⁻¹ * x * g = n⁻¹ * x * n
theorem sylow.conj_eq_normalizer_conj_of_mem {p : } {G : Type u_1} [group G] [fact (nat.prime p)] [finite (sylow p G)] (P : G) [hP : P.is_commutative] (x g : G) (hx : x P) (hy : g⁻¹ * x * g P) :
(n : G) (H : n P.normalizer), g⁻¹ * x * g = n⁻¹ * x * n
noncomputable 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
@[protected, instance]
noncomputable def has_quotient.quotient.fintype {p : } {G : Type u_1} [group G] [fact (nat.prime p)] [fintype (sylow p G)] (P : G) :
Equations
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 not_dvd_index_sylow' {p : } {G : Type u_1} [group G] [hp : fact (nat.prime p)] (P : G) [P.normal] [P.finite_index] :
theorem not_dvd_index_sylow {p : } {G : Type u_1} [group G] [hp : fact (nat.prime p)] [finite (sylow p G)] (P : G) (hP : 0) :
theorem sylow.normalizer_sup_eq_top {G : Type u_1} [group G] {p : } [fact (nat.prime p)] {N : subgroup G} [N.normal] [finite (sylow p N)] (P : N) :

Frattini's Argument: If N is a normal subgroup of G, and if P is a Sylow p-subgroup of N, then N_G(P) ⊔ N = G.

theorem sylow.normalizer_sup_eq_top' {G : Type u_1} [group G] {p : } [fact (nat.prime p)] {N : subgroup G} [N.normal] [finite (sylow p N)] (P : G) (hP : P N) :

Frattini's Argument: If N is a normal subgroup of G, and if P is a Sylow p-subgroup of N, then N_G(P) ⊔ N = G.

theorem quotient_group.card_preimage_mk {G : Type u} [group G] [fintype G] (s : subgroup G) (t : set (G s)) :

The fixed points of the action of H on its cosets correspond to normalizer H / H.

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

theorem sylow.pow_dvd_card_of_pow_dvd_card {G : Type u} [group G] [fintype G] {p n : } [hp : fact (nat.prime p)] (P : G) (hdvd : p ^ n ) :
p ^ n
theorem sylow.dvd_card_of_dvd_card {G : Type u} [group G] [fintype G] {p : } [fact (nat.prime p)] (P : G) (hdvd : p ) :
theorem sylow.card_coprime_index {G : Type u} [group G] [fintype G] {p : } [hp : fact (nat.prime p)] (P : G) :

Sylow subgroups are Hall subgroups.

theorem sylow.ne_bot_of_dvd_card {G : Type u} [group G] [fintype G] {p : } [hp : fact (nat.prime p)] (P : G) (hdvd : p ) :
theorem sylow.card_eq_multiplicity {G : Type u} [group G] [fintype G] {p : } [hp : fact (nat.prime p)] (P : G) :

The cardinality of a Sylow subgroup is p ^ n where n is the multiplicity of p in the group order.

def sylow.of_card {G : Type u} [group G] [fintype G] {p : } [hp : fact (nat.prime p)] (H : subgroup G) [fintype H] (card_eq : = p ^ ((fintype.card G).factorization) p) :
G

A subgroup with cardinality p ^ n is a Sylow subgroup where n is the multiplicity of p in the group order.

Equations
@[simp, norm_cast]
theorem sylow.coe_of_card {G : Type u} [group G] [fintype G] {p : } [hp : fact (nat.prime p)] (H : subgroup G) [fintype H] (card_eq : = p ^ ((fintype.card G).factorization) p) :
card_eq) = H
theorem sylow.subsingleton_of_normal {G : Type u} [group G] {p : } [fact (nat.prime p)] [finite (sylow p G)] (P : G) (h : P.normal) :
theorem sylow.characteristic_of_normal {G : Type u} [group G] {p : } [fact (nat.prime p)] [finite (sylow p G)] (P : G) (h : P.normal) :
theorem sylow.normal_of_normalizer_normal {G : Type u} [group G] {p : } [fact (nat.prime p)] [finite (sylow p G)] (P : G) (hn : P.normalizer.normal) :
@[simp]
theorem sylow.normalizer_normalizer {G : Type u} [group G] {p : } [fact (nat.prime p)] [finite (sylow p G)] (P : G) :
theorem sylow.normal_of_all_max_subgroups_normal {G : Type u} [group G] [finite G] (hnc : (H : subgroup G), H.normal) {p : } [fact (nat.prime p)] [finite (sylow p G)] (P : G) :
theorem sylow.normal_of_normalizer_condition {G : Type u} [group G] (hnc : normalizer_condition G) {p : } [fact (nat.prime p)] [finite (sylow p G)] (P : G) :
noncomputable def sylow.direct_product_of_normal {G : Type u} [group G] [fintype G] (hn : {p : } [_inst_3 : fact (nat.prime p)] (P : G), P.normal) :
(Π (p : .support)) (P : G), P) ≃* G

If all its Sylow subgroups are normal, then a finite group is isomorphic to the direct product of these Sylow subgroups.

Equations