The p-core and the 2-core O₂(G) (Stage A)

This file builds the machinery of the p-core Oₚ(G) — the largest normal p-subgroup of G — and specialises it to the 2-core O₂(G), the wild subgroup that controls the Q₂ presentation.

Mathlib (as of this toolchain) has no pCore / Fitting-subgroup API, so we define it here as the join (sSup) of all normal p-subgroups and develop the interface used by the rest of the formalisation:

• pCore, twoCore — the definitions;
• pCore_normal / twoCore_normal — normality (any group);
• pCore_isPGroup — for a finite group the join really is a p-group (the substantive lemma: a finite directed join of normal p-subgroups, proved by Finset.sup_induction);
• normal_pSubgroup_le_pCore — maximality;
• mem_twoCore_iff_normal_closure_is_two_group — the characterisation used in Proposition 2.3 (current_manuscript, §2): a single element lies in O₂(G) iff the normal closure it generates is a 2-group;
• hom_image_twoCore_le_twoCore — functoriality under surjections (the epimorphism sends the wild subgroup into the target 2-core);
• quotient_by_twoCore_has_no_nontrivial_normal_two_subgroup — O₂(G/O₂(G)) = 1, the fact that makes the wild subgroup characteristic (Lemma 3.3 / lem:o2tame).

All proofs are constructive and sorry-free; the p-group facts come from Mathlib.GroupTheory.PGroup.

def Q2Presentation.pCore (p : ℕ) (G : Type u_1) [Group G] : Subgroup G

The p-core Oₚ(G): the join of all normal p-subgroups of G.

For a finite group this is the unique largest normal p-subgroup (pCore_isPGroup, normal_pSubgroup_le_pCore). The definition itself makes sense for any group, and normality holds unconditionally (pCore_normal).

Equations

• Q2Presentation.pCore p G = sSup {N : Subgroup G | N.Normal ∧ IsPGroup p ↥N}

@[reducible, inline]

abbrev Q2Presentation.twoCore (G : Type u_1) [Group G] : Subgroup G

The 2-core O₂(G) — the wild subgroup of the Q₂ presentation.

Equations

• Q2Presentation.twoCore G = Q2Presentation.pCore 2 G

theorem Q2Presentation.pCore_normal (p : ℕ) (G : Type u_1) [Group G] : (pCore p G).Normal

The p-core is normal (in any group): a join of normal subgroups is normal.

instance Q2Presentation.instNormalPCore (p : ℕ) (G : Type u_1) [Group G] : (pCore p G).Normal

theorem Q2Presentation.normal_pSubgroup_le_pCore {p : ℕ} {G : Type u_1} [Group G] {N : Subgroup G} (hN : N.Normal) (h2 : IsPGroup p ↥N) : N ≤ pCore p G

Maximality: every normal p-subgroup is contained in the p-core.

theorem Q2Presentation.pCore_mem {p : ℕ} {G : Type u_1} [Group G] [Finite G] : (pCore p G).Normal ∧ IsPGroup p ↥(pCore p G)

For a finite group, the p-core is itself a normal p-subgroup.

The join of all normal p-subgroups is a finite supremum (there are finitely many subgroups), and the class of normal p-subgroups is closed under binary join (IsPGroup.to_sup_of_normal_right + Subgroup.sup_normal) and contains ⊥; Finset.sup_induction then propagates the property to the whole join.

theorem Q2Presentation.pCore_isPGroup {p : ℕ} {G : Type u_1} [Group G] [Finite G] : IsPGroup p ↥(pCore p G)

For a finite group the p-core is a p-group.

theorem Q2Presentation.mem_pCore_iff_normalClosure_isPGroup {p : ℕ} {G : Type u_1} [Group G] [Finite G] {x : G} : x ∈ pCore p G ↔ IsPGroup p ↥(Subgroup.normalClosure {x})

Characterisation of membership: x ∈ Oₚ(G) iff the normal closure of x is a p-group. This is the finite-target criterion behind Proposition 2.3.

theorem Q2Presentation.map_pCore_le_pCore_of_surjective {p : ℕ} {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (φ : G →* H) (hφ : Function.Surjective ⇑φ) : Subgroup.map φ (pCore p G) ≤ pCore p H

Functoriality under surjections: a surjective homomorphism carries the p-core into the p-core of the target. (Its image is a normal p-subgroup.)

theorem Q2Presentation.pCore_quotient_eq_bot {p : ℕ} {G : Type u_1} [Group G] [Finite G] : pCore p (G ⧸ pCore p G) = ⊥

Oₚ(G / Oₚ(G)) = 1: the quotient by the p-core has no nontrivial normal p-subgroup. Equivalently, the p-core is idempotent in the sense that passing to the quotient annihilates it.

The 2-core interface

The four lemmas named in the Stage A specification, specialised to p = 2.

theorem Q2Presentation.twoCore_normal (G : Type u_1) [Group G] : (twoCore G).Normal

The 2-core is normal.

theorem Q2Presentation.twoCore_isPGroup {G : Type u_1} [Group G] [Finite G] : IsPGroup 2 ↥(twoCore G)

For a finite group the 2-core is a 2-group.

theorem Q2Presentation.mem_twoCore_iff_normal_closure_is_two_group {G : Type u_1} [Group G] [Finite G] {x : G} : x ∈ twoCore G ↔ IsPGroup 2 ↥(Subgroup.normalClosure {x})

x ∈ O₂(G) iff the normal closure of x is a 2-group.

theorem Q2Presentation.hom_image_twoCore_le_twoCore {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (φ : G →* H) (hφ : Function.Surjective ⇑φ) : Subgroup.map φ (twoCore G) ≤ twoCore H

A surjection carries the 2-core into the target 2-core (functoriality): the image of the wild subgroup under an epimorphism lands in O₂ of the target.

theorem Q2Presentation.quotient_by_twoCore_has_no_nontrivial_normal_two_subgroup (G : Type u_1) [Group G] [Finite G] (N : Subgroup (G ⧸ twoCore G)) (hN : N.Normal) (h2 : IsPGroup 2 ↥N) : N = ⊥

The quotient by the 2-core has no nontrivial normal 2-subgroup, i.e. O₂(G / O₂(G)) = 1. This is what makes the wild subgroup characteristic (lem:o2tame).