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) [Group G] extends Subgroup : Type u_1

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

• carrier : Set G
• mul_mem' : ∀ {a b : G}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier
• inv_mem' : ∀ {x : G}, x ∈ self.carrier → x⁻¹ ∈ self.carrier
• isPGroup' : IsPGroup p ↥↑self
• is_maximal' : ∀ {Q : Subgroup G}, IsPGroup p ↥Q → ↑self ≤ Q → Q = ↑self

instance Sylow.instCoeOutSylowSubgroup {p : ℕ} {G : Type u_1} [Group G] : CoeOut (Sylow p G) (Subgroup G)

Equations

• Sylow.instCoeOutSylowSubgroup = { coe := Sylow.toSubgroup }

theorem Sylow.ext {p : ℕ} {G : Type u_1} [Group G] {P : Sylow p G} {Q : Sylow p G} (h : ↑P = ↑Q) : P = Q

theorem Sylow.ext_iff {p : ℕ} {G : Type u_1} [Group G] {P : Sylow p G} {Q : Sylow p G} : P = Q ↔ ↑P = ↑Q

instance Sylow.instSetLikeSylow {p : ℕ} {G : Type u_1} [Group G] : SetLike (Sylow p G) G

Equations

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

instance Sylow.instSubgroupClassSylowToDivInvMonoidInstSetLikeSylow {p : ℕ} {G : Type u_1} [Group G] : SubgroupClass (Sylow p G) G

Equations

• (_ : SubgroupClass (Sylow p G) G) = (_ : SubgroupClass (Sylow p G) G)

instance Sylow.mulActionLeft {p : ℕ} {G : Type u_1} [Group G] (P : Sylow p G) {α : Type u_2} [MulAction G α] : MulAction (↥↑P) α

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

Equations

• Sylow.mulActionLeft P = inferInstanceAs (MulAction (↥↑P) α)

def Sylow.comapOfKerIsPGroup {p : ℕ} {G : Type u_1} [Group G] (P : Sylow p G) {K : Type u_2} [Group K] (ϕ : K →* G) (hϕ : IsPGroup p ↥(MonoidHom.ker ϕ)) (h : ↑P ≤ MonoidHom.range ϕ) : Sylow p K

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

Equations

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

@[simp]

theorem Sylow.coe_comapOfKerIsPGroup {p : ℕ} {G : Type u_1} [Group G] (P : Sylow p G) {K : Type u_2} [Group K] (ϕ : K →* G) (hϕ : IsPGroup p ↥(MonoidHom.ker ϕ)) (h : ↑P ≤ MonoidHom.range ϕ) : ↑(Sylow.comapOfKerIsPGroup P ϕ hϕ h) = Subgroup.comap ϕ ↑P

def Sylow.comapOfInjective {p : ℕ} {G : Type u_1} [Group G] (P : Sylow p G) {K : Type u_2} [Group K] (ϕ : K →* G) (hϕ : Function.Injective ⇑ϕ) (h : ↑P ≤ MonoidHom.range ϕ) : Sylow p K

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

Equations

• Sylow.comapOfInjective P ϕ hϕ h = Sylow.comapOfKerIsPGroup P ϕ (_ : IsPGroup p ↥(MonoidHom.ker ϕ)) h

@[simp]

theorem Sylow.coe_comapOfInjective {p : ℕ} {G : Type u_1} [Group G] (P : Sylow p G) {K : Type u_2} [Group K] (ϕ : K →* G) (hϕ : Function.Injective ⇑ϕ) (h : ↑P ≤ MonoidHom.range ϕ) : ↑(Sylow.comapOfInjective P ϕ hϕ h) = Subgroup.comap ϕ ↑P

def Sylow.subtype {p : ℕ} {G : Type u_1} [Group G] (P : Sylow p G) {N : Subgroup G} (h : ↑P ≤ N) : Sylow p ↥N

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

Equations

• Sylow.subtype P h = Sylow.comapOfInjective P (Subgroup.subtype N) (_ : Function.Injective fun (a : ↥N) => ↑a) (_ : ↑P ≤ MonoidHom.range (Subgroup.subtype N))

@[simp]

theorem Sylow.coe_subtype {p : ℕ} {G : Type u_1} [Group G] (P : Sylow p G) {N : Subgroup G} (h : ↑P ≤ N) : ↑(Sylow.subtype P h) = Subgroup.subgroupOf (↑P) N

theorem Sylow.subtype_injective {p : ℕ} {G : Type u_1} [Group G] {N : Subgroup G} {P : Sylow p G} {Q : Sylow p G} {hP : ↑P ≤ N} {hQ : ↑Q ≤ N} (h : Sylow.subtype P hP = Sylow.subtype Q hQ) : P = Q

theorem IsPGroup.exists_le_sylow {p : ℕ} {G : Type u_1} [Group G] {P : Subgroup G} (hP : IsPGroup 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 Sylow.nonempty {p : ℕ} {G : Type u_1} [Group G] : Nonempty (Sylow p G)

Equations

• (_ : Nonempty (Sylow p G)) = (_ : Nonempty (Sylow p G))

noncomputable instance Sylow.inhabited {p : ℕ} {G : Type u_1} [Group G] : Inhabited (Sylow p G)

Equations

• Sylow.inhabited = Classical.inhabited_of_nonempty (_ : Nonempty (Sylow p G))

theorem Sylow.exists_comap_eq_of_ker_isPGroup {p : ℕ} {G : Type u_1} [Group G] {H : Type u_2} [Group H] (P : Sylow p H) {f : H →* G} (hf : IsPGroup p ↥(MonoidHom.ker f)) : ∃ (Q : Sylow p G), Subgroup.comap f ↑Q = ↑P

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) : ∃ (Q : Sylow p G), Subgroup.comap f ↑Q = ↑P

theorem Sylow.exists_comap_subtype_eq {p : ℕ} {G : Type u_1} [Group G] {H : Subgroup G} (P : Sylow p ↥H) : ∃ (Q : Sylow p G), Subgroup.comap (Subgroup.subtype H) ↑Q = ↑P

noncomputable def Sylow.fintypeOfKerIsPGroup {p : ℕ} {G : Type u_1} [Group G] {H : Type u_2} [Group H] {f : H →* G} (hf : IsPGroup p ↥(MonoidHom.ker f)) [Fintype (Sylow p G)] : Fintype (Sylow p H)

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

Equations

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

noncomputable def Sylow.fintypeOfInjective {p : ℕ} {G : Type u_1} [Group G] {H : Type u_2} [Group H] {f : H →* G} (hf : Function.Injective ⇑f) [Fintype (Sylow p G)] : Fintype (Sylow p H)

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

Equations

• Sylow.fintypeOfInjective hf = Sylow.fintypeOfKerIsPGroup (_ : IsPGroup p ↥(MonoidHom.ker f))

noncomputable instance instFintypeSylowSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupToGroup {p : ℕ} {G : Type u_1} [Group G] (H : Subgroup G) [Fintype (Sylow p G)] : Fintype (Sylow p ↥H)

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

Equations

• instFintypeSylowSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupToGroup H = Sylow.fintypeOfInjective (_ : Function.Injective ⇑(Subgroup.subtype H))

instance instFiniteSylowSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupToGroup {p : ℕ} {G : Type u_1} [Group G] (H : Subgroup G) [Finite (Sylow p G)] : Finite (Sylow p ↥H)

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

Equations

• (_ : Finite (Sylow p ↥H)) = (_ : Finite (Sylow p ↥H))

instance Sylow.pointwiseMulAction {p : ℕ} {G : Type u_1} [Group G] {α : Type u_2} [Group α] [MulDistribMulAction α G] : MulAction α (Sylow p G)

Subgroup.pointwiseMulAction preserves Sylow subgroups.

Equations

• Sylow.pointwiseMulAction = MulAction.mk (_ : ∀ (P : Sylow p G), 1 • P = P) (_ : ∀ (g h : α) (P : Sylow p G), (g * h) • P = g • h • P)

theorem Sylow.pointwise_smul_def {p : ℕ} {G : Type u_1} [Group G] {α : Type u_2} [Group α] [MulDistribMulAction α G] {g : α} {P : Sylow p G} : ↑(g • P) = g • ↑P

instance Sylow.mulAction {p : ℕ} {G : Type u_1} [Group G] : MulAction G (Sylow p G)

Equations

• Sylow.mulAction = MulAction.compHom (Sylow p G) MulAut.conj

theorem Sylow.smul_def {p : ℕ} {G : Type u_1} [Group G] {g : G} {P : Sylow p G} : g • P = MulAut.conj g • P

theorem Sylow.coe_subgroup_smul {p : ℕ} {G : Type u_1} [Group G] {g : G} {P : Sylow p G} : ↑(g • P) = MulAut.conj g • ↑P

theorem Sylow.coe_smul {p : ℕ} {G : Type u_1} [Group G] {g : G} {P : Sylow p G} : ↑(g • P) = MulAut.conj g • ↑P

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 • Sylow.subtype P hP = Sylow.subtype (h • P) (_ : ↑(h • P) ≤ H)

theorem Sylow.smul_eq_iff_mem_normalizer {p : ℕ} {G : Type u_1} [Group G] {g : G} {P : Sylow p G} : g • P = P ↔ g ∈ Subgroup.normalizer ↑P

theorem Sylow.smul_eq_of_normal {p : ℕ} {G : Type u_1} [Group G] {g : G} {P : Sylow p G} [h : Subgroup.Normal ↑P] : g • P = P

theorem Subgroup.sylow_mem_fixedPoints_iff {p : ℕ} {G : Type u_1} [Group G] (H : Subgroup G) {P : Sylow p G} : P ∈ MulAction.fixedPoints (↥H) (Sylow p G) ↔ H ≤ Subgroup.normalizer ↑P

theorem IsPGroup.inf_normalizer_sylow {p : ℕ} {G : Type u_1} [Group G] {P : Subgroup G} (hP : IsPGroup p ↥P) (Q : Sylow p G) : P ⊓ Subgroup.normalizer ↑Q = P ⊓ ↑Q

theorem IsPGroup.sylow_mem_fixedPoints_iff {p : ℕ} {G : Type u_1} [Group G] {P : Subgroup G} (hP : IsPGroup p ↥P) {Q : Sylow p G} : Q ∈ MulAction.fixedPoints (↥P) (Sylow p G) ↔ P ≤ ↑Q

instance instIsPretransitiveSylowToSMulToMonoidToDivInvMonoidMulAction {p : ℕ} {G : Type u_1} [Group G] [hp : Fact (Nat.Prime p)] [Finite (Sylow p G)] : MulAction.IsPretransitive 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.

Equations

• (_ : MulAction.IsPretransitive G (Sylow p G)) = (_ : MulAction.IsPretransitive G (Sylow p G))

theorem card_sylow_modEq_one (p : ℕ) (G : Type u_1) [Group G] [Fact (Nat.Prime p)] [Fintype (Sylow p G)] : Fintype.card (Sylow p G) ≡ 1 [MOD p]

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)] : ¬p ∣ Fintype.card (Sylow p G)

def Sylow.equivSMul {p : ℕ} {G : Type u_1} [Group G] (P : Sylow p G) (g : G) : ↥↑P ≃* ↥↑(g • P)

Sylow subgroups are isomorphic

Equations

• Sylow.equivSMul P g = Subgroup.equivSMul (MulAut.conj g) ↑P

noncomputable def Sylow.equiv {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) (Q : Sylow p G) : ↥↑P ≃* ↥↑Q

Sylow subgroups are isomorphic

Equations

• Sylow.equiv P Q = Eq.mpr (_ : (↥↑P ≃* ↥↑Q) = (↥↑P ≃* ↥↑(Classical.choose (_ : ∃ (m : G), m • P = Q) • P))) (Sylow.equivSMul P (Classical.choose (_ : ∃ (m : G), m • P = Q)))

@[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) : MulAction.orbit G P = ⊤

theorem Sylow.stabilizer_eq_normalizer {p : ℕ} {G : Type u_1} [Group G] (P : Sylow p G) : MulAction.stabilizer G P = Subgroup.normalizer ↑P

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 : G) (hx : x ∈ Subgroup.centralizer ↑P) (hy : g⁻¹ * x * g ∈ Subgroup.centralizer ↑P) : ∃ n ∈ Subgroup.normalizer ↑P, 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 : Subgroup.IsCommutative ↑P] (x : G) (g : G) (hx : x ∈ P) (hy : g⁻¹ * x * g ∈ P) : ∃ n ∈ Subgroup.normalizer ↑P, g⁻¹ * x * g = n⁻¹ * x * n

noncomputable def Sylow.equivQuotientNormalizer {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Fintype (Sylow p G)] (P : Sylow p G) : Sylow p G ≃ G ⧸ Subgroup.normalizer ↑P

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.

noncomputable instance instFintypeQuotientSubgroupInstHasQuotientSubgroupNormalizerToSubgroup {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Fintype (Sylow p G)] (P : Sylow p G) : Fintype (G ⧸ Subgroup.normalizer ↑P)

Equations

• instFintypeQuotientSubgroupInstHasQuotientSubgroupNormalizerToSubgroup P = Fintype.ofEquiv (Sylow p G) (Sylow.equivQuotientNormalizer P)

theorem card_sylow_eq_card_quotient_normalizer {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Fintype (Sylow p G)] (P : Sylow p G) : Fintype.card (Sylow p G) = Fintype.card (G ⧸ Subgroup.normalizer ↑P)

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) : Fintype.card (Sylow p G) = Subgroup.index (Subgroup.normalizer ↑P)

theorem card_sylow_dvd_index {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Fintype (Sylow p G)] (P : Sylow p G) : Fintype.card (Sylow p G) ∣ Subgroup.index ↑P

theorem not_dvd_index_sylow' {p : ℕ} {G : Type u_1} [Group G] [hp : Fact (Nat.Prime p)] (P : Sylow p G) [Subgroup.Normal ↑P] [fP : Subgroup.FiniteIndex ↑P] : ¬p ∣ Subgroup.index ↑P

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 : Subgroup.relindex (↑P) (Subgroup.normalizer ↑P) ≠ 0) : ¬p ∣ Subgroup.index ↑P

theorem Sylow.normalizer_sup_eq_top {G : Type u_1} [Group G] {p : ℕ} [Fact (Nat.Prime p)] {N : Subgroup G} [Subgroup.Normal N] [Finite (Sylow p ↥N)] (P : Sylow p ↥N) : Subgroup.normalizer (Subgroup.map (Subgroup.subtype 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} [Subgroup.Normal N] [Finite (Sylow p ↥N)] (P : Sylow p G) (hP : ↑P ≤ N) : Subgroup.normalizer ↑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 QuotientGroup.card_preimage_mk {G : Type u} [Group G] [Fintype G] (s : Subgroup G) (t : Set (G ⧸ s)) : Fintype.card ↑(QuotientGroup.mk ⁻¹' t) = Fintype.card ↥s * Fintype.card ↑t

theorem Sylow.mem_fixedPoints_mul_left_cosets_iff_mem_normalizer {G : Type u} [Group G] {H : Subgroup G} [Finite ↑↑H] {x : G} : ↑x ∈ MulAction.fixedPoints (↥H) (G ⧸ H) ↔ x ∈ Subgroup.normalizer H

def Sylow.fixedPointsMulLeftCosetsEquivQuotient {G : Type u} [Group G] (H : Subgroup G) [Finite ↑↑H] : ↑(MulAction.fixedPoints (↥H) (G ⧸ H)) ≃ ↥(Subgroup.normalizer H) ⧸ Subgroup.comap (Subgroup.subtype (Subgroup.normalizer H)) H

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

Equations

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

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 : Fintype.card ↥H = p ^ n) : Fintype.card (↥(Subgroup.normalizer H) ⧸ Subgroup.comap (Subgroup.subtype (Subgroup.normalizer H)) H) ≡ Fintype.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} [Group G] [Fintype G] {p : ℕ} {n : ℕ} [hp : Fact (Nat.Prime p)] {H : Subgroup G} (hH : Fintype.card ↥H = p ^ n) : Fintype.card ↥(Subgroup.normalizer H) ≡ Fintype.card G [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) ∣ Fintype.card G) {H : Subgroup G} (hH : Fintype.card ↥H = p ^ n) : p ∣ Fintype.card (↥(Subgroup.normalizer H) ⧸ Subgroup.comap (Subgroup.subtype (Subgroup.normalizer H)) 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} [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) : p ^ (n + 1) ∣ Fintype.card ↥(Subgroup.normalizer H)

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

theorem Sylow.exists_subgroup_card_pow_prime_of_le_card {G : Type u} [Group G] {n : ℕ} {p : ℕ} (hp : Nat.Prime p) (h : IsPGroup p G) (hn : p ^ n ≤ Nat.card G) : ∃ (H : Subgroup G), Nat.card ↥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} [Group G] {n : ℕ} {p : ℕ} (hp : Nat.Prime p) (h : IsPGroup p G) {H : Subgroup G} (hn : p ^ n ≤ Nat.card ↥H) : ∃ H' ≤ H, Nat.card ↥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} [Group G] {k : ℕ} {p : ℕ} (hp : Nat.Prime p) (h : IsPGroup p G) {H : Subgroup G} (hk : k ≤ Nat.card ↥H) (hk₀ : k ≠ 0) : ∃ H' ≤ H, Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥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} [Group G] [Fintype G] {p : ℕ} {n : ℕ} [hp : Fact (Nat.Prime p)] (P : Sylow p G) (hdvd : p ^ n ∣ Fintype.card G) : p ^ n ∣ Fintype.card ↥↑P

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) : p ∣ Fintype.card ↥↑P

theorem Sylow.card_coprime_index {G : Type u} [Group G] [Fintype G] {p : ℕ} [hp : Fact (Nat.Prime p)] (P : Sylow p G) : Nat.Coprime (Fintype.card ↥↑P) (Subgroup.index ↑P)

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) : ↑P ≠ ⊥

theorem Sylow.card_eq_multiplicity {G : Type u} [Group G] [Fintype G] {p : ℕ} [hp : Fact (Nat.Prime p)] (P : Sylow p G) : Fintype.card ↥↑P = p ^ (Nat.factorization (Fintype.card G)) 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} [Group G] [Fintype G] {p : ℕ} [Fact (Nat.Prime p)] (H : Subgroup G) [Fintype ↥H] (card_eq : Fintype.card ↥H = p ^ (Nat.factorization (Fintype.card G)) 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' := (_ : IsPGroup p ↥H), is_maximal' := (_ : ∀ {Q : Subgroup G}, IsPGroup p ↥Q → H ≤ Q → Q = H) }

@[simp]

theorem Sylow.coe_ofCard {G : Type u} [Group G] [Fintype G] {p : ℕ} [Fact (Nat.Prime p)] (H : Subgroup G) [Fintype ↥H] (card_eq : Fintype.card ↥H = p ^ (Nat.factorization (Fintype.card G)) p) : ↑(Sylow.ofCard H card_eq) = H

noncomputable def Sylow.unique_of_normal {G : Type u} [Group G] {p : ℕ} [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) (h : Subgroup.Normal ↑P) : Unique (Sylow p G)

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

Equations

• Sylow.unique_of_normal P h = { toInhabited := Sylow.inhabited, uniq := (_ : ∀ (Q : Sylow p G), Q = default) }

theorem Sylow.characteristic_of_normal {G : Type u} [Group G] {p : ℕ} [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) (h : Subgroup.Normal ↑P) : Subgroup.Characteristic ↑P

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 : Subgroup.Normal (Subgroup.normalizer ↑P)) : Subgroup.Normal ↑P

@[simp]

theorem Sylow.normalizer_normalizer {G : Type u} [Group G] {p : ℕ} [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) : Subgroup.normalizer (Subgroup.normalizer ↑P) = Subgroup.normalizer ↑P

theorem Sylow.normal_of_all_max_subgroups_normal {G : Type u} [Group G] [Finite G] (hnc : ∀ (H : Subgroup G), IsCoatom H → Subgroup.Normal H) {p : ℕ} [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) : Subgroup.Normal ↑P

theorem Sylow.normal_of_normalizerCondition {G : Type u} [Group G] (hnc : NormalizerCondition G) {p : ℕ} [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) : Subgroup.Normal ↑P

noncomputable def Sylow.directProductOfNormal {G : Type u} [Group G] [Fintype G] (hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Subgroup.Normal ↑P) : ((p : { x : ℕ // x ∈ (Fintype.card G).primeFactors }) → (P : Sylow (↑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

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