Sylow Theorems

Statement

Let $G$ be a finite group and $p$ a prime. Write $|G| = p^a m$ with $\gcd(p, m) = 1$.

• Sylow I: A subgroup of order $p^a$ exists (called a Sylow $p$-subgroup). More generally, for every $k \leq a$, $G$ has a subgroup of order $p^k$.
• Sylow II: All Sylow $p$-subgroups are conjugate to each other.
• Sylow III: The number $n_p$ of Sylow $p$-subgroups satisfies $n_p \equiv 1 \pmod{p}$ and $n_p \mid m$.

Visualization

Take $G = A_5$, the alternating group on 5 letters, with $|A_5| = 60 = 2^2 \cdot 3 \cdot 5$.

Factorisation of 60:
  60 = 4 × 15  (p=2, a=2, m=15)
  60 = 3 × 20  (p=3, a=1, m=20)
  60 = 5 × 12  (p=5, a=1, m=12)

Sylow subgroups of $A_5$:

Prime p=2: Sylow 2-subgroups have order 4 (≅ Z/2×Z/2, Klein four-groups)
  n_2 ≡ 1 (mod 2) and n_2 | 15  →  n_2 ∈ {1,3,5,15}
  Actual count: n_2 = 5

Prime p=3: Sylow 3-subgroups have order 3 (≅ Z/3, generated by 3-cycles)
  n_3 ≡ 1 (mod 3) and n_3 | 20  →  n_3 ∈ {1,4,10}
  Actual count: n_3 = 10

Prime p=5: Sylow 5-subgroups have order 5 (≅ Z/5, generated by 5-cycles)
  n_5 ≡ 1 (mod 5) and n_5 | 12  →  n_5 ∈ {1,6}
  Actual count: n_5 = 6

No Sylow $p$-subgroup is normal in $A_5$ (all counts $> 1$) — which is precisely the footprint of $A_5$ being simple!

Element type count check ($|A_5| = 60$):

identity:          1
3-cycles (in P_3): 10 × 2 = 20  (each Z/3 contributes 2 non-identity)
5-cycles (in P_5):  6 × 4 = 24  (each Z/5 contributes 4 non-identity)
double transpositions: 15
Total: 1 + 20 + 24 + 15 = 60  ✓

Proof Sketch

Sylow I uses a counting argument: embed $G \hookrightarrow S_{|G|}$ (Cayley), then exhibit subgroups of $S_{p^a m}$ of order $p^a$, and apply a fixed-point count modulo $p$.

Sylow II follows from the fact that every $p$-subgroup fixes a point in the action of $G$ on the set of Sylow $p$-subgroups by conjugation, forcing all Sylow subgroups into the same orbit.

Sylow III counts the orbit of any Sylow $p$-subgroup $P$ under conjugation: the stabilizer of $P$ contains $P$ itself, so $|$orbit$| = [G : N_G(P)]$ divides $m$. The congruence $n_p \equiv 1 \pmod{p}$ is a fixed-point theorem for the action of $P$ on Sylow subgroups.

Connections

Sylow theorems are the converse direction of Lagrange's TheoremLagrange's Theorem$$|H| \;\text{divides}\; |G|$$Subgroup order divides group orderRead more → — Lagrange says subgroup orders divide $|G|$; Sylow says prime-power divisors actually produce subgroups. They are the main tool for classifying groups of small order and for the group-theoretic step in the Impossibility of the Quintic FormulaImpossibility of the Quintic Formula$$S_5 \text{ is not solvable} \implies \text{no radical formula for degree } \geq 5$$No general algebraic formula exists for polynomials of degree 5 or higherRead more → (showing $A_5$ has no proper normal subgroups). Cauchy's Theorem (Groups)Cauchy's Theorem (Groups)$$p \mid |G| \implies \exists g \in G,\; \operatorname{ord}(g) = p$$If a prime p divides |G| then G has an element of order pRead more → is the $k=1$ special case of Sylow I. The conjugacy results resemble the orbit-stabilizer structure underlying the Fundamental Theorem of Galois TheoryFundamental Theorem of Galois Theory$$\{\text{intermediate fields}\} \longleftrightarrow \{\text{subgroups of } \text{Gal}(K/F)\}$$Bijection between intermediate fields and subgroups of the Galois groupRead more →.

/-- **Sylow's First Theorem**: for every prime-power divisor p^n of |G|,
    there exists a subgroup of order p^n.
    Mathlib: `Sylow.exists_subgroup_card_pow_prime`
    in `Mathlib.GroupTheory.Sylow`. -/
theorem sylow_first {G : Type*} [Group G] [Finite G] (p : ℕ) [Fact p.Prime]
    {n : ℕ} (h : p ^ n ∣ Nat.card G) :
    ∃ K : Subgroup G, Nat.card K = p ^ n :=
  Sylow.exists_subgroup_card_pow_prime p h

/-- **Sylow's Second Theorem**: all Sylow p-subgroups are conjugate.
    Two elements of `Sylow p G` are always conjugate in G.
    Mathlib: `Sylow.isPretransitive_of_prime` / `MulAction.IsPretransitive`
    on the conjugation action captures transitivity. -/
example {G : Type*} [Group G] [Fintype G] (p : ℕ) [Fact p.Prime] :
    MulAction.IsPretransitive G (Sylow p G) :=
  inferInstance