mathlib3 documentation

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.

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.

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 : 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
@[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 : sylow p G) {α : Type u_2} [mul_action G α] :

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 : sylow p G) {K : Type u_2} [group K] (ϕ : K →* G) (hϕ : is_p_group p (ϕ.ker)) (h : P ϕ.range) :
sylow p 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 : sylow p G) {K : Type u_2} [group K] (ϕ : K →* G) (hϕ : is_p_group p (ϕ.ker)) (h : P ϕ.range) :
def sylow.comap_of_injective {p : } {G : Type u_1} [group G] (P : sylow p G) {K : Type u_2} [group K] (ϕ : K →* G) (hϕ : function.injective ϕ) (h : P ϕ.range) :
sylow p K

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

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

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

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

@[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 : sylow p H) {f : H →* G} (hf : is_p_group p (f.ker)) :
theorem sylow.exists_comap_eq_of_injective {p : } {G : Type u_1} [group G] {H : Type u_2} [group H] (P : sylow p H) {f : H →* G} (hf : function.injective f) :
theorem sylow.exists_comap_subtype_eq {p : } {G : Type u_1} [group G] {H : subgroup G} (P : sylow p H) :
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 : is_p_group p (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 α] [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
@[protected, 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_le {p : } {G : Type u_1} [group G] {P : sylow 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 : sylow 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 : sylow p G} :
theorem sylow.smul_eq_of_normal {p : } {G : Type u_1} [group G] {g : G} {P : sylow p G} [h : P.normal] :
g P = P
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} :
@[protected, instance]

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 : sylow 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 : sylow p 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 : sylow 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 : sylow p G) (x g : G) (hx : x subgroup.centralizer P) (hy : g⁻¹ * x * g subgroup.centralizer P) :
(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 : sylow 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 : sylow 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 : sylow 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 : 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 not_dvd_index_sylow' {p : } {G : Type u_1} [group G] [hp : fact (nat.prime p)] (P : sylow 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 : sylow p G) (hP : P.relindex P.normalizer 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 : sylow 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 : sylow 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.

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) :

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 : sylow p G) (hdvd : p ^ n fintype.card G) :
theorem sylow.dvd_card_of_dvd_card {G : Type u} [group G] [fintype G] {p : } [fact (nat.prime p)] (P : sylow p G) (hdvd : p fintype.card G) :
theorem sylow.card_coprime_index {G : Type u} [group G] [fintype G] {p : } [hp : fact (nat.prime p)] (P : sylow 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 : sylow p G) (hdvd : p fintype.card G) :
theorem sylow.card_eq_multiplicity {G : Type u} [group G] [fintype G] {p : } [hp : fact (nat.prime p)] (P : sylow 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 : fintype.card H = p ^ ((fintype.card G).factorization) p) :
sylow 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 : fintype.card H = p ^ ((fintype.card G).factorization) p) :
(sylow.of_card H card_eq) = H
theorem sylow.subsingleton_of_normal {G : Type u} [group G] {p : } [fact (nat.prime p)] [finite (sylow p G)] (P : sylow 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 : sylow 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 : sylow 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 : sylow p G) :
theorem sylow.normal_of_all_max_subgroups_normal {G : Type u} [group G] [finite G] (hnc : (H : subgroup G), is_coatom H H.normal) {p : } [fact (nat.prime p)] [finite (sylow p G)] (P : sylow 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 : sylow 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 : sylow p G), P.normal) :

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

Equations