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 ofG. - All Sylow
p-subgroups ofGare conjugate to each other. - Let
nₚbe the number of Sylowp-subgroups ofG, thennₚdivides the index of the Sylowp-subgroup,nₚ ≡ 1 [MOD p], andnₚis equal to the index of the normalizer of the Sylowp-subgroup inG.
Main definitions #
sylow p G: The type of Sylowp-subgroups ofG.
Main statements #
exists_subgroup_card_pow_prime: A generalization of Sylow's first theorem: For every prime powerpⁿdividing the cardinality ofG, there exists a subgroup ofGof orderpⁿ.is_p_group.exists_le_sylow: A generalization of Sylow's first theorem: Everyp-subgroup is contained in a Sylowp-subgroup.sylow_conjugate: A generalization of Sylow's second theorem: If the number of Sylowp-subgroups is finite, then all Sylowp-subgroups are conjugate.card_sylow_modeq_one: A generalization of Sylow's third theorem: If the number of Sylowp-subgroups is finite, then it is congruent to1modulop.
- to_subgroup : subgroup G
- is_p_group' : is_p_group p ↥(self.to_subgroup)
- is_maximal' : ∀ {Q : subgroup G}, is_p_group p ↥Q → self.to_subgroup ≤ Q → Q = self.to_subgroup
A Sylow p-subgroup is a maximal p-subgroup.
@[protected, instance]
Equations
- sylow.subgroup.has_coe = {coe := sylow.to_subgroup _inst_1}
@[simp]
theorem
sylow.to_subgroup_eq_coe
{p : ℕ}
{G : Type u_1}
[group G]
{P : sylow p G} :
P.to_subgroup = ↑P
@[protected, instance]
Equations
- sylow.set_like = {coe := coe coe_to_lift, coe_injective' := _}
theorem
is_p_group.exists_le_sylow
{p : ℕ}
{G : Type u_1}
[group G]
{P : subgroup G}
(hP : is_p_group p ↥P) :
A generalization of Sylow's first theorem.
Every p-subgroup is contained in a Sylow p-subgroup.
@[protected, instance]
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)) :
∃ (Q : sylow p G), subgroup.comap f Q.to_subgroup = ↑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.to_subgroup = ↑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 H.subtype Q.to_subgroup = ↑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 : 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
- sylow.fintype_of_ker_is_p_group hf = let h_exists : ∀ (P : sylow p H), ∃ (Q : sylow p G), subgroup.comap f Q.to_subgroup = ↑P := _, g : sylow p H → sylow p G := λ (P : sylow p H), classical.some _, hg : ∀ (P : sylow p H), subgroup.comap f (g P).to_subgroup = ↑P := _ in fintype.of_injective g _
@[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
- sylow.pointwise_mul_action = {to_has_scalar := {smul := λ (g : α) (P : sylow p G), {to_subgroup := g • ↑P, is_p_group' := _, is_maximal' := _}}, one_smul := _, mul_smul := _}
@[protected, instance]
Equations
theorem
sylow.smul_def
{p : ℕ}
{G : Type u_1}
[group G]
{g : G}
{P : sylow p G} :
g • P = ⇑mul_aut.conj g • P
theorem
subgroup.sylow_mem_fixed_points_iff
{p : ℕ}
{G : Type u_1}
[group G]
(H : subgroup G)
{P : sylow p G} :
P ∈ mul_action.fixed_points ↥H (sylow p G) ↔ H ≤ ↑P.normalizer
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]
def
sylow.mul_action.is_pretransitive
{p : ℕ}
{G : Type u_1}
[group G]
[hp : fact (nat.prime p)]
[fintype (sylow p G)] :
mul_action.is_pretransitive 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.
Sylow subgroups are isomorphic
Equations
- P.equiv_smul g = subgroup.equiv_smul (⇑mul_aut.conj g) P.to_subgroup
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 G ≃ G ⧸ P.to_subgroup.normalizer
Sylow p-subgroups are in bijection with cosets of the normalizer of a Sylow p-subgroup
Equations
- P.equiv_quotient_normalizer = (((equiv.set.univ (sylow p G)).symm.trans (_.mpr (equiv.refl ↥⊤))).trans (mul_action.orbit_equiv_quotient_stabilizer G P)).trans (_.mpr (equiv.refl (G ⧸ P.to_subgroup.normalizer)))
@[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) :
fintype (G ⧸ P.to_subgroup.normalizer)
Equations
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 ⧸ P.to_subgroup.normalizer)
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) = P.to_subgroup.normalizer.index
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) ∣ P.to_subgroup.index
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) :
(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
quotient_group.card_preimage_mk
{G : Type u}
[group G]
[fintype G]
(s : subgroup G)
(t : set (G ⧸ s)) :
fintype.card ↥(quotient_group.mk ⁻¹' t) = (fintype.card ↥s) * fintype.card ↥t
theorem
sylow.mem_fixed_points_mul_left_cosets_iff_mem_normalizer
{G : Type u}
[group G]
{H : subgroup G}
[fintype ↥↑H]
{x : G} :
↑x ∈ mul_action.fixed_points ↥H (G ⧸ H) ↔ x ∈ H.normalizer
def
sylow.fixed_points_mul_left_cosets_equiv_quotient
{G : Type u}
[group G]
(H : subgroup G)
[fintype ↥↑H] :
↥(mul_action.fixed_points ↥H (G ⧸ H)) ≃ ↥(H.normalizer) ⧸ subgroup.comap H.normalizer.subtype H
Equations
- sylow.fixed_points_mul_left_cosets_equiv_quotient H = equiv.subtype_quotient_equiv_quotient_subtype ↑(H.normalizer) (mul_action.fixed_points ↥H (quotient (id {r := λ (x y : G), x⁻¹ * y ∈ H, iseqv := _}))) _ _
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 (↥(H.normalizer) ⧸ subgroup.comap H.normalizer.subtype 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 ↥(H.normalizer) ≡ 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 (↥(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}
[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 ↥(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}
[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 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) :
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.pow_dvd_card_of_pow_dvd_card
{G : Type u}
[group G]
[fintype G]
{p n : ℕ}
[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_eq_multiplicity
{G : Type u}
[group G]
[fintype G]
{p : ℕ}
[hp : fact (nat.prime p)]
(P : sylow p G) :
fintype.card ↥P = p ^ ⇑((fintype.card G).factorization) p
The cardinality of a Sylow group is p ^ n
where n is the multiplicity of p in the group order.
def
sylow.comap_of_ker_is_p_group
{G : Type u}
[group G]
{p : ℕ}
(P : sylow p G)
{K : Type u_1}
[group K]
(ϕ : K →* G)
(hϕ : is_p_group p ↥(ϕ.ker))
(h : P.to_subgroup ≤ ϕ.range) :
sylow p K
The preimage of a Sylow subgroup under a homomorphism with p-group-kernel is a Sylow subgroup
Equations
- P.comap_of_ker_is_p_group ϕ hϕ h = {to_subgroup := {carrier := (subgroup.comap ϕ P.to_subgroup).carrier, one_mem' := _, mul_mem' := _, inv_mem' := _}, is_p_group' := _, is_maximal' := _}
@[simp]
theorem
sylow.coe_comap_of_ker_is_p_group
{G : Type u}
[group G]
{p : ℕ}
{P : sylow p G}
{K : Type u_1}
[group K]
(ϕ : K →* G)
(hϕ : is_p_group p ↥(ϕ.ker))
(h : P.to_subgroup ≤ ϕ.range) :
↑(P.comap_of_ker_is_p_group ϕ hϕ h) = subgroup.comap ϕ ↑P
def
sylow.comap_of_injective
{G : Type u}
[group G]
{p : ℕ}
(P : sylow p G)
{K : Type u_1}
[group K]
(ϕ : K →* G)
(hϕ : function.injective ⇑ϕ)
(h : P.to_subgroup ≤ ϕ.range) :
sylow p K
The preimage of a Sylow subgroup under an injective homomorphism is a Sylow subgroup
Equations
- P.comap_of_injective ϕ hϕ h = P.comap_of_ker_is_p_group ϕ _ h
@[simp]
theorem
sylow.coe_comap_of_injective
{G : Type u}
[group G]
{p : ℕ}
{P : sylow p G}
{K : Type u_1}
[group K]
(ϕ : K →* G)
(hϕ : function.injective ⇑ϕ)
(h : P.to_subgroup ≤ ϕ.range) :
↑(P.comap_of_injective ϕ hϕ h) = subgroup.comap ϕ ↑P
@[simp]
theorem
sylow.coe_subtype
{G : Type u}
[group G]
{p : ℕ}
{P : sylow p G}
{N : subgroup G}
{h : P.to_subgroup ≤ N} :