Composition series of finite p-groups

TheoremComposition series of finite p-groups#✓fully proved

Let \(p\) be a prime and let \(G\) be a finite \(p\)-group of order \(p^n\). Then there are subgroups \(G = H_0 \supseteq H_1 \supseteq \cdots \supseteq H_n = \{1\}\) such that for each \(i < n\), \(H_{i+1}\) is a normal subgroup of \(H_i\) and there is a surjective homomorphism \(H_i \to \mathbb{Z}/p\mathbb{Z}\) with kernel \(H_{i+1}\). By the first isomorphism theorem, \(H_i / H_{i+1} \cong \mathbb{Z}/p\mathbb{Z}\) for each \(i < n\).

theorem exists_chain_zmod_p_quotients (hG : IsPGroup p G) {n : ℕ}
    (hn : Nat.card G = p ^ n) :
    ∃ H : Fin (n + 1) → Subgroup G,
      H 0 = ⊤ ∧
        H (Fin.last n) = ⊥ ∧
        ∀ i : Fin n,
          H i.succ ≤ H i.castSucc ∧
            ((H i.succ).subgroupOf (H i.castSucc)).Normal ∧
            ∃ φ : ↥(H i.castSucc) →* Multiplicative (ZMod p),
              Function.Surjective φ ∧ φ.ker = (H i.succ).subgroupOf (H i.castSucc)

TheoremFinite p-groups are solvable#✓fully proved

For every prime \(p\), every finite \(p\)-group is solvable.

theorem isSolvable (hG : IsPGroup p G) : Group.IsSolvable G

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.