# 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ⁿ.
• IsPGroup.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) [] extends :
Type u_1

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

• carrier : Set G
• mul_mem' : ∀ {a b : G}, a (↑self).carrierb (↑self).carriera * b (↑self).carrier
• one_mem' : 1 (↑self).carrier
• inv_mem' : ∀ {x : G}, x (↑self).carrierx⁻¹ (↑self).carrier
• isPGroup' : IsPGroup p { x : G // x self }
• is_maximal' : ∀ {Q : }, IsPGroup p { x : G // x Q }self QQ = self
Instances For
theorem Sylow.isPGroup' {p : } {G : Type u_1} [] (self : Sylow p G) :
IsPGroup p { x : G // x self }
theorem Sylow.is_maximal' {p : } {G : Type u_1} [] (self : Sylow p G) {Q : } :
IsPGroup p { x : G // x Q }self QQ = self
instance Sylow.instCoeOutSubgroup {p : } {G : Type u_1} [] :
Equations
• Sylow.instCoeOutSubgroup = { coe := Sylow.toSubgroup }
theorem Sylow.ext_iff {p : } {G : Type u_1} [] {P : Sylow p G} {Q : Sylow p G} :
P = Q P = Q
theorem Sylow.ext {p : } {G : Type u_1} [] {P : Sylow p G} {Q : Sylow p G} (h : P = Q) :
P = Q
instance Sylow.instSetLike {p : } {G : Type u_1} [] :
SetLike (Sylow p G) G
Equations
• Sylow.instSetLike = { coe := fun (x : Sylow p G) => x, coe_injective' := }
instance Sylow.instSubgroupClass {p : } {G : Type u_1} [] :
Equations
• =
instance Sylow.mulActionLeft {p : } {G : Type u_1} [] (P : Sylow p G) {α : Type u_2} [] :
MulAction { x : G // x P } α

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

Equations
def Sylow.comapOfKerIsPGroup {p : } {G : Type u_1} [] (P : Sylow p G) {K : Type u_2} [] (ϕ : K →* G) (hϕ : IsPGroup p { x : K // x ϕ.ker }) (h : P ϕ.range) :
Sylow p K

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

Equations
• P.comapOfKerIsPGroup ϕ h = { toSubgroup := , isPGroup' := , is_maximal' := }
Instances For
@[simp]
theorem Sylow.coe_comapOfKerIsPGroup {p : } {G : Type u_1} [] (P : Sylow p G) {K : Type u_2} [] (ϕ : K →* G) (hϕ : IsPGroup p { x : K // x ϕ.ker }) (h : P ϕ.range) :
(P.comapOfKerIsPGroup ϕ h) =
def Sylow.comapOfInjective {p : } {G : Type u_1} [] (P : Sylow p G) {K : Type u_2} [] (ϕ : K →* G) (hϕ : ) (h : P ϕ.range) :
Sylow p K

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

Equations
• P.comapOfInjective ϕ h = P.comapOfKerIsPGroup ϕ h
Instances For
@[simp]
theorem Sylow.coe_comapOfInjective {p : } {G : Type u_1} [] (P : Sylow p G) {K : Type u_2} [] (ϕ : K →* G) (hϕ : ) (h : P ϕ.range) :
(P.comapOfInjective ϕ h) =
def Sylow.subtype {p : } {G : Type u_1} [] (P : Sylow p G) {N : } (h : P N) :
Sylow p { x : G // x N }

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

Equations
• P.subtype h = P.comapOfInjective N.subtype
Instances For
@[simp]
theorem Sylow.coe_subtype {p : } {G : Type u_1} [] (P : Sylow p G) {N : } (h : P N) :
(P.subtype h) = (↑P).subgroupOf N
theorem Sylow.subtype_injective {p : } {G : Type u_1} [] {N : } {P : Sylow p G} {Q : Sylow p G} {hP : P N} {hQ : Q N} (h : P.subtype hP = Q.subtype hQ) :
P = Q
theorem IsPGroup.exists_le_sylow {p : } {G : Type u_1} [] {P : } (hP : IsPGroup p { x : G // x 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 Sylow.nonempty {p : } {G : Type u_1} [] :
Equations
• =
noncomputable instance Sylow.inhabited {p : } {G : Type u_1} [] :
Equations
• Sylow.inhabited =
theorem Sylow.exists_comap_eq_of_ker_isPGroup {p : } {G : Type u_1} [] {H : Type u_2} [] (P : Sylow p H) {f : H →* G} (hf : IsPGroup p { x : H // x f.ker }) :
∃ (Q : Sylow p G), = P
theorem Sylow.exists_comap_eq_of_injective {p : } {G : Type u_1} [] {H : Type u_2} [] (P : Sylow p H) {f : H →* G} (hf : ) :
∃ (Q : Sylow p G), = P
theorem Sylow.exists_comap_subtype_eq {p : } {G : Type u_1} [] {H : } (P : Sylow p { x : G // x H }) :
∃ (Q : Sylow p G), Subgroup.comap H.subtype Q = P
theorem Sylow.finite_of_ker_is_pGroup {p : } {G : Type u_1} [] {H : Type u_2} [] {f : H →* G} (hf : IsPGroup p { x : H // x f.ker }) [Finite (Sylow p G)] :

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

theorem Sylow.finite_of_injective {p : } {G : Type u_1} [] {H : Type u_2} [] {f : H →* G} (hf : ) [Finite (Sylow p G)] :

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

instance instFiniteSylowSubtypeMemSubgroup {p : } {G : Type u_1} [] (H : ) [Finite (Sylow p G)] :
Finite (Sylow p { x : G // x H })

If H is a subgroup of G, then Finite (Sylow p G) implies Finite (Sylow p H).

Equations
• =
instance Sylow.pointwiseMulAction {p : } {G : Type u_1} [] {α : Type u_2} [] [] :
MulAction α (Sylow p G)

Subgroup.pointwiseMulAction preserves Sylow subgroups.

Equations
• Sylow.pointwiseMulAction =
theorem Sylow.pointwise_smul_def {p : } {G : Type u_1} [] {α : Type u_2} [] [] {g : α} {P : Sylow p G} :
(g P) = g P
instance Sylow.mulAction {p : } {G : Type u_1} [] :
Equations
theorem Sylow.smul_def {p : } {G : Type u_1} [] {g : G} {P : Sylow p G} :
g P = MulAut.conj g P
theorem Sylow.coe_subgroup_smul {p : } {G : Type u_1} [] {g : G} {P : Sylow p G} :
(g P) = MulAut.conj g P
theorem Sylow.coe_smul {p : } {G : Type u_1} [] {g : G} {P : Sylow p G} :
(g P) = MulAut.conj g P
theorem Sylow.smul_le {p : } {G : Type u_1} [] {P : Sylow p G} {H : } (hP : P H) (h : { x : G // x H }) :
(h P) H
theorem Sylow.smul_subtype {p : } {G : Type u_1} [] {P : Sylow p G} {H : } (hP : P H) (h : { x : G // x H }) :
h P.subtype hP = (h P).subtype
theorem Sylow.smul_eq_iff_mem_normalizer {p : } {G : Type u_1} [] {g : G} {P : Sylow p G} :
g P = P g (↑P).normalizer
theorem Sylow.smul_eq_of_normal {p : } {G : Type u_1} [] {g : G} {P : Sylow p G} [h : (↑P).Normal] :
g P = P
theorem Subgroup.sylow_mem_fixedPoints_iff {p : } {G : Type u_1} [] (H : ) {P : Sylow p G} :
P MulAction.fixedPoints { x : G // x H } (Sylow p G) H (↑P).normalizer
theorem IsPGroup.inf_normalizer_sylow {p : } {G : Type u_1} [] {P : } (hP : IsPGroup p { x : G // x P }) (Q : Sylow p G) :
P (↑Q).normalizer = P Q
theorem IsPGroup.sylow_mem_fixedPoints_iff {p : } {G : Type u_1} [] {P : } (hP : IsPGroup p { x : G // x P }) {Q : Sylow p G} :
Q MulAction.fixedPoints { x : G // x P } (Sylow p G) P Q
instance instIsPretransitiveSylowOfFactPrimeOfFinite {p : } {G : Type u_1} [] [hp : Fact (Nat.Prime p)] [Finite (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.

Equations
• =
theorem card_sylow_modEq_one (p : ) (G : Type u_1) [] [Fact (Nat.Prime p)] [Finite (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) [] [hp : Fact (Nat.Prime p)] [Finite (Sylow p G)] :
def Sylow.equivSMul {p : } {G : Type u_1} [] (P : Sylow p G) (g : G) :
{ x : G // x P } ≃* { x : G // x (g P) }

Sylow subgroups are isomorphic

Equations
Instances For
noncomputable def Sylow.equiv {p : } {G : Type u_1} [] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) (Q : Sylow p G) :
{ x : G // x P } ≃* { x : G // x Q }

Sylow subgroups are isomorphic

Equations
• P.equiv Q = .mpr (P.equivSMul )
Instances For
@[simp]
theorem Sylow.orbit_eq_top {p : } {G : Type u_1} [] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
theorem Sylow.stabilizer_eq_normalizer {p : } {G : Type u_1} [] (P : Sylow p G) :
= (↑P).normalizer
theorem Sylow.conj_eq_normalizer_conj_of_mem_centralizer {p : } {G : Type u_1} [] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) (x : G) (g : G) (hx : ) (hy : g⁻¹ * x * g ) :
n(↑P).normalizer, g⁻¹ * x * g = n⁻¹ * x * n
theorem Sylow.conj_eq_normalizer_conj_of_mem {p : } {G : Type u_1} [] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) [_hP : (↑P).IsCommutative] (x : G) (g : G) (hx : x P) (hy : g⁻¹ * x * g P) :
n(↑P).normalizer, g⁻¹ * x * g = n⁻¹ * x * n
noncomputable def Sylow.equivQuotientNormalizer {p : } {G : Type u_1} [] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
Sylow p G G (↑P).normalizer

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance instFiniteQuotientSubgroupNormalizerOfFactPrimeOfSylow {p : } {G : Type u_1} [] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
Finite (G (↑P).normalizer)
Equations
• =
theorem card_sylow_eq_card_quotient_normalizer {p : } {G : Type u_1} [] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
Nat.card (Sylow p G) = Nat.card (G (↑P).normalizer)
theorem card_sylow_eq_index_normalizer {p : } {G : Type u_1} [] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
Nat.card (Sylow p G) = (↑P).normalizer.index
theorem card_sylow_dvd_index {p : } {G : Type u_1} [] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
Nat.card (Sylow p G) (↑P).index
theorem not_dvd_index_sylow' {p : } {G : Type u_1} [] [hp : Fact (Nat.Prime p)] (P : Sylow p G) [(↑P).Normal] [fP : (↑P).FiniteIndex] :
¬p (↑P).index
theorem not_dvd_index_sylow {p : } {G : Type u_1} [] [hp : Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) (hP : (↑P).relindex (↑P).normalizer 0) :
¬p (↑P).index
theorem Sylow.normalizer_sup_eq_top {G : Type u_1} [] {p : } [Fact (Nat.Prime p)] {N : } [N.Normal] [Finite (Sylow p { x : G // x N })] (P : Sylow p { x : G // x N }) :
(Subgroup.map N.subtype P).normalizer 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} [] {p : } [Fact (Nat.Prime p)] {N : } [N.Normal] [Finite (Sylow p { x : G // x N })] (P : Sylow p G) (hP : P N) :
(↑P).normalizer 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 QuotientGroup.card_preimage_mk {G : Type u} [] (s : ) (t : Set (G s)) :
Nat.card (QuotientGroup.mk ⁻¹' t) = Nat.card { x : G // x s } * Nat.card t
theorem Sylow.mem_fixedPoints_mul_left_cosets_iff_mem_normalizer {G : Type u} [] {H : } [Finite H] {x : G} :
x MulAction.fixedPoints { x : G // x H } (G H) x H.normalizer
def Sylow.fixedPointsMulLeftCosetsEquivQuotient {G : Type u} [] (H : ) [Finite H] :
(MulAction.fixedPoints { x : G // x H } (G H)) { x : G // x H.normalizer } Subgroup.comap H.normalizer.subtype H

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

Equations
Instances For
theorem Sylow.card_quotient_normalizer_modEq_card_quotient {G : Type u} [] [] {p : } {n : } [hp : Fact (Nat.Prime p)] {H : } (hH : Nat.card { x : G // x H } = p ^ n) :
Nat.card ({ x : G // x H.normalizer } Subgroup.comap H.normalizer.subtype H) Nat.card (G H) [MOD p]

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} [] [] {p : } {n : } [hp : Fact (Nat.Prime p)] {H : } (hH : Nat.card { x : G // x H } = p ^ n) :
Nat.card { x : G // x H.normalizer } [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} [] [] {p : } {n : } [hp : Fact (Nat.Prime p)] (hdvd : p ^ (n + 1) ) {H : } (hH : Nat.card { x : G // x H } = p ^ n) :
p Nat.card ({ x : G // x H.normalizer } Subgroup.comap H.normalizer.subtype H)

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} [] [] {p : } {n : } [_hp : Fact (Nat.Prime p)] (hdvd : p ^ (n + 1) ) {H : } (hH : Nat.card { x : G // x H } = p ^ n) :
p ^ (n + 1) Nat.card { x : G // x H.normalizer }

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} [] [] {p : } {n : } [hp : Fact (Nat.Prime p)] (hdvd : p ^ (n + 1) ) {H : } (hH : Nat.card { x : G // x H } = p ^ n) :
∃ (K : ), Nat.card { x : G // x 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

@[irreducible]
theorem Sylow.exists_subgroup_card_pow_prime_le {G : Type u} [] [] (p : ) {n : } {m : } [_hp : Fact (Nat.Prime p)] (_hdvd : p ^ m ) (H : ) (_hH : Nat.card { x : G // x H } = p ^ n) (_hnm : n m) :
∃ (K : ), Nat.card { x : G // x 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} [] [] (p : ) {n : } [Fact (Nat.Prime p)] (hdvd : p ^ n ) :
∃ (K : ), Nat.card { x : G // x 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

theorem Sylow.exists_subgroup_card_pow_prime_of_le_card {G : Type u} [] {n : } {p : } (hp : ) (h : IsPGroup p G) (hn : p ^ n ) :
∃ (H : ), Nat.card { x : G // x H } = p ^ n

A special case of Sylow's first theorem. If G is a p-group of size at least p ^ n then there is a subgroup of cardinality p ^ n.

theorem Sylow.exists_subgroup_le_card_pow_prime_of_le_card {G : Type u} [] {n : } {p : } (hp : ) (h : IsPGroup p G) {H : } (hn : p ^ n Nat.card { x : G // x H }) :
H'H, Nat.card { x : G // x H' } = p ^ n

A special case of Sylow's first theorem. If G is a p-group and H a subgroup of size at least p ^ n then there is a subgroup of H of cardinality p ^ n.

theorem Sylow.exists_subgroup_le_card_le {G : Type u} [] {k : } {p : } (hp : ) (h : IsPGroup p G) {H : } (hk : k Nat.card { x : G // x H }) (hk₀ : k 0) :
H'H, Nat.card { x : G // x H' } k k < p * Nat.card { x : G // x H' }

A special case of Sylow's first theorem. If G is a p-group and H a subgroup of size at least k then there is a subgroup of H of cardinality between k / p and k.

theorem Sylow.pow_dvd_card_of_pow_dvd_card {G : Type u} [] [] {p : } {n : } [hp : Fact (Nat.Prime p)] (P : Sylow p G) (hdvd : p ^ n ) :
p ^ n Nat.card { x : G // x P }
theorem Sylow.dvd_card_of_dvd_card {G : Type u} [] [] {p : } [Fact (Nat.Prime p)] (P : Sylow p G) (hdvd : p ) :
p Nat.card { x : G // x P }
theorem Sylow.card_coprime_index {G : Type u} [] [] {p : } [hp : Fact (Nat.Prime p)] (P : Sylow p G) :
(Nat.card { x : G // x P }).Coprime (↑P).index

Sylow subgroups are Hall subgroups.

theorem Sylow.ne_bot_of_dvd_card {G : Type u} [] [] {p : } [hp : Fact (Nat.Prime p)] (P : Sylow p G) (hdvd : p ) :
P
theorem Sylow.card_eq_multiplicity {G : Type u} [] [] {p : } [hp : Fact (Nat.Prime p)] (P : Sylow p G) :
Nat.card { x : G // x P } = p ^ (Nat.card G).factorization p

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

def Sylow.ofCard {G : Type u} [] [] {p : } [Fact (Nat.Prime p)] (H : ) (card_eq : Nat.card { x : G // x H } = p ^ (Nat.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
• Sylow.ofCard H card_eq = { toSubgroup := H, isPGroup' := , is_maximal' := }
Instances For
@[simp]
theorem Sylow.coe_ofCard {G : Type u} [] [] {p : } [Fact (Nat.Prime p)] (H : ) (card_eq : Nat.card { x : G // x H } = p ^ (Nat.card G).factorization p) :
(Sylow.ofCard H card_eq) = H
noncomputable def Sylow.unique_of_normal {G : Type u} [] {p : } [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) (h : (↑P).Normal) :

If G has a normal Sylow p-subgroup, then it is the only Sylow p-subgroup.

Equations
• P.unique_of_normal h = { toInhabited := Sylow.inhabited, uniq := }
Instances For
theorem Sylow.characteristic_of_normal {G : Type u} [] {p : } [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) (h : (↑P).Normal) :
(↑P).Characteristic
theorem Sylow.normal_of_normalizer_normal {G : Type u} [] {p : } [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) (hn : (↑P).normalizer.Normal) :
(↑P).Normal
@[simp]
theorem Sylow.normalizer_normalizer {G : Type u} [] {p : } [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
(↑P).normalizer.normalizer = (↑P).normalizer
theorem Sylow.normal_of_all_max_subgroups_normal {G : Type u} [] [] (hnc : ∀ (H : ), H.Normal) {p : } [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
(↑P).Normal
theorem Sylow.normal_of_normalizerCondition {G : Type u} [] (hnc : ) {p : } [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
(↑P).Normal
noncomputable def Sylow.directProductOfNormal {G : Type u} [] [] (hn : ∀ {p : } [inst : Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal) :
((p : { x : // x (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → { x : G // x P }) ≃* G

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

Equations
• One or more equations did not get rendered due to their size.
Instances For