Sylow subgroups and conjugacy of prime-power order elements

When a prime p divides the order of a group exactly once, its Sylow p-subgroups have order p. This is the form in which Sylow's theorems are applied to groups such as S₅, whose order 120 is divisible by 5 but not by 25, and to their subgroups.

The file also records that p times the number of Sylow p-subgroups divides the order of the group whenever p does. When p ^ 2 does not divide the order, any two elements of order p generate conjugate subgroups. More generally, every element of prime-power order is conjugate to an element of any chosen Sylow subgroup for that prime.

Main results

• Sylow.exists_isConj_of_orderOf_dvd_pow: an element of prime-power order has a conjugate in any chosen Sylow subgroup.
• Sylow.card_eq_of_dvd_of_not_sq_dvd: a Sylow p-subgroup has order p when p divides the order of the group but p ^ 2 does not.
• Sylow.mul_card_sylow_dvd_card: if p divides the order of the group, then so does p times the number of Sylow p-subgroups.
• TauCeti.exists_mul_mul_inv_mem_zpowers_of_not_sq_dvd: if p ^ 2 does not divide the order of the group, some conjugate of an element of order p is a power of any other element of order p.

theorem Sylow.exists_isConj_of_orderOf_dvd_pow {G : Type u_1} [Group G] {p : ℕ} [hp : Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) {g : G} {n : ℕ} (hg : orderOf g ∣ p ^ n) : ∃ (x : ↥P), IsConj (↑x) g

Every element of prime-power order is conjugate to an element of any chosen Sylow subgroup for that prime. Only finiteness of the set of Sylow subgroups is needed.

theorem Sylow.card_eq_of_dvd_of_not_sq_dvd {G : Type u_1} [Group G] {p : ℕ} [hp : Fact (Nat.Prime p)] (P : Sylow p G) (hdvd : p ∣ Nat.card G) (hsq : ¬p ^ 2 ∣ Nat.card G) : Nat.card ↥↑P = p

A Sylow p-subgroup has order p when p divides the order of the group exactly once.

theorem Sylow.mul_card_sylow_dvd_card {G : Type u_1} [Group G] {p : ℕ} [hp : Fact (Nat.Prime p)] (hdvd : p ∣ Nat.card G) : p * Nat.card (Sylow p G) ∣ Nat.card G

If a prime p divides the order of a group, then so does p times the number of Sylow p-subgroups.

theorem TauCeti.exists_mul_mul_inv_mem_zpowers_of_not_sq_dvd {G : Type u_1} [Group G] {p : ℕ} [hp : Fact (Nat.Prime p)] (hsq : ¬p ^ 2 ∣ Nat.card G) {g h : G} (hg : orderOf g = p) (hh : orderOf h = p) : ∃ (y : G), y * h * y⁻¹ ∈ Subgroup.zpowers g

If p ^ 2 does not divide the order of a group, then the subgroups generated by two elements of order p are Sylow p-subgroups, hence conjugate: some conjugate of h is a power of g.