feat(GroupTheory/PCore): define the p-core of a subgroup

Mathlib.lean

@@ -4755,6 +4755,7 @@ public import Mathlib.GroupTheory.OrderOfElement
 public import Mathlib.GroupTheory.OreLocalization.Basic
 public import Mathlib.GroupTheory.OreLocalization.Cardinality
 public import Mathlib.GroupTheory.OreLocalization.OreSet
+public import Mathlib.GroupTheory.PCore
 public import Mathlib.GroupTheory.PGroup
 public import Mathlib.GroupTheory.Perm.Basic
 public import Mathlib.GroupTheory.Perm.Centralizer

Mathlib/Algebra/Group/Subgroup/Pointwise.lean

@@ -381,6 +381,17 @@ instance sup_normal (H K : Subgroup G) [hH : H.Normal] [hK : K.Normal] : (H ⊔
     refine ⟨g * h * g⁻¹, hH.conj_mem h hh g, g * k * g⁻¹, hK.conj_mem k hk g, ?_⟩
     simp only [mul_assoc, inv_mul_cancel_left]
 
+@[to_additive]
+theorem normal_iSup_normal {ι : Sort*} {a : ι → Subgroup G}
+    (norm : ∀ i : ι, (a i).Normal) : (iSup a).Normal where
+  conj_mem x hx g := by
+    refine iSup_induction (C := fun x => g * x * g⁻¹ ∈ iSup a) a hx ?_ ?_ ?_
+    · intro i y hy
+      exact mem_iSup_of_mem i ((norm i).conj_mem y hy g)
+    · simp
+    · intro y z hy hz
+      simpa only [mul_assoc, inv_mul_cancel_left] using mul_mem hy hz
+
 @[to_additive]
 theorem smul_mem_of_mem_closure_of_mem {X : Type*} [MulAction G X] {s : Set G} {t : Set X}
     (hs : ∀ g ∈ s, g⁻¹ ∈ s) (hst : ∀ᵉ (g ∈ s) (x ∈ t), g • x ∈ t) {g : G}

Mathlib/GroupTheory/PCore.lean

@@ -0,0 +1,207 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+public import Mathlib.GroupTheory.Sylow
+
+/-!
+# The `p`-core of a group
+
+For a group `G` and a natural number `p`, the **`p`-core** `O_p(G)` is the
+largest normal `p`-subgroup of `G`. We define it as the supremum of all
+normal `p`-subgroups, prove that it is normal, and prove that it is itself
+a `p`-group (no finiteness hypothesis needed: the family of normal
+`p`-subgroups is directed under `≤`).
+
+## Main definitions
+
+* `Subgroup.pCore p G` : the `p`-core of `G`, classically denoted `O_p(G)`.
+
+## Main results
+
+* `Subgroup.pCore_normal` (instance), `Subgroup.isPGroup_pCore`:
+  `pCore p G` is a normal `p`-subgroup, with no finiteness hypothesis.
+* `Subgroup.normal_le_pCore`: for `N` normal in `G`, `N ≤ pCore p G ↔ IsPGroup p N`
+  — the universal property.
+* `Subgroup.pCore_eq_iInf_sylow`: `pCore p G = ⨅ P : Sylow p G, (P : Subgroup G)`.
+* `Subgroup.comap_pCore_eq_pCore`, `MulEquiv.map_pCore`, and surrounding
+  lemmas describe the behaviour of `pCore` under group homomorphisms.
+
+## TODO
+
+* Interaction with `IsSolvable` and the upper Fitting series.
+-/
+
+public section
+
+namespace Subgroup
+
+open scoped Pointwise
+
+variable {G : Type*} [Group G] {p : ℕ}
+
+/-- The **`p`-core** `O_p(G)` of a group `G`: the supremum of all normal
+`p`-subgroups. By `isPGroup_pCore` this is itself a `p`-group, and so is
+the largest normal `p`-subgroup of `G`.
+
+We define it via an `iSup` over the subtype of normal `p`-subgroups,
+which makes `Subgroup.iSup_induction` directly applicable. -/
+@[expose] def pCore (p : ℕ) (G : Type*) [Group G] : Subgroup G :=
+  ⨆ N : {N : Subgroup G // N.Normal ∧ IsPGroup p N}, (N : Subgroup G)
+
+/-- The subtype of normal `p`-subgroups is nonempty (it contains `⊥`). -/
+private instance : Nonempty {N : Subgroup G // N.Normal ∧ IsPGroup p N} :=
+  ⟨⟨⊥, inferInstance, IsPGroup.of_bot⟩⟩
+
+/-- Every normal `p`-subgroup of `G` is contained in the `p`-core. -/
+theorem le_pCore {N : Subgroup G} (hN_normal : N.Normal) (hN_pGroup : IsPGroup p N) :
+    N ≤ pCore p G :=
+  le_iSup (fun N : {N : Subgroup G // N.Normal ∧ IsPGroup p N} => (N : Subgroup G))
+    ⟨N, hN_normal, hN_pGroup⟩
+
+/-- The `p`-core is normal in `G`. -/
+instance pCore_normal : (pCore p G).Normal :=
+  normal_iSup_normal fun N => N.2.1
+
+/-- The indexing family of normal `p`-subgroups is directed under `≤`:
+for any two normal `p`-subgroups, their join is again a normal
+`p`-subgroup. -/
+theorem directed_pCore :
+    Directed (· ≤ ·)
+      (fun N : {N : Subgroup G // N.Normal ∧ IsPGroup p N} => (N : Subgroup G)) := by
+  rintro ⟨N₁, h₁N, h₁P⟩ ⟨N₂, h₂N, h₂P⟩
+  haveI := h₁N
+  haveI := h₂N
+  exact ⟨⟨N₁ ⊔ N₂, sup_normal N₁ N₂, h₁P.to_sup_of_normal_left h₂P⟩,
+    le_sup_left, le_sup_right⟩
+
+/-- The `p`-core is itself a `p`-group. Since the family of normal
+`p`-subgroups is directed under `≤`, every element of the supremum
+already lies in one of them. -/
+theorem isPGroup_pCore : IsPGroup p (pCore p G) := by
+  intro ⟨x, hx⟩
+  obtain ⟨N, hxN⟩ := (mem_iSup_of_directed directed_pCore).mp hx
+  obtain ⟨k, hk⟩ := N.2.2 ⟨x, hxN⟩
+  refine ⟨k, ?_⟩
+  ext
+  simpa using Subtype.ext_iff.mp hk
+
+/-- For a normal subgroup `N` of `G`, containment in the `p`-core is
+characterised by being a `p`-group. -/
+theorem normal_le_pCore {N : Subgroup G} [hN : N.Normal] :
+    N ≤ pCore p G ↔ IsPGroup p N :=
+  ⟨fun h => isPGroup_pCore.to_le h, le_pCore hN⟩
+
+/-- Characterisation of membership in the `p`-core: an element lies in
+`pCore p G` iff it lies in some normal `p`-subgroup of `G`. -/
+theorem mem_pCore_iff {x : G} :
+    x ∈ pCore p G ↔ ∃ N : Subgroup G, N.Normal ∧ IsPGroup p N ∧ x ∈ N := by
+  rw [pCore, mem_iSup_of_directed directed_pCore]
+  exact ⟨fun ⟨N, hxN⟩ => ⟨N, N.2.1, N.2.2, hxN⟩,
+    fun ⟨N, hN, hP, hxN⟩ => ⟨⟨N, hN, hP⟩, hxN⟩⟩
+
+/-- The `p`-core is trivial iff `G` has no non-trivial normal `p`-subgroup. -/
+theorem pCore_eq_bot_iff :
+    pCore p G = ⊥ ↔ ∀ N : Subgroup G, N.Normal → IsPGroup p N → N = ⊥ := by
+  refine ⟨fun h N hN hP => le_bot_iff.mp (h ▸ le_pCore hN hP), fun h => ?_⟩
+  rw [eq_bot_iff_forall]
+  intro x hx
+  obtain ⟨N, hN, hP, hxN⟩ := mem_pCore_iff.mp hx
+  simpa [h N hN hP] using hxN
+
+/-- `pCore p G = ⊤` iff the whole group `G` is a `p`-group. -/
+theorem pCore_eq_top_iff : pCore p G = ⊤ ↔ IsPGroup p (⊤ : Subgroup G) :=
+  ⟨fun h => isPGroup_pCore.to_le (h ▸ le_rfl), fun h => eq_top_iff.2 (le_pCore inferInstance h)⟩
+
+/-- If `G` itself is a `p`-group, then `pCore p G = ⊤`. -/
+theorem pCore_eq_top (h : IsPGroup p (⊤ : Subgroup G)) : pCore p G = ⊤ :=
+  pCore_eq_top_iff.2 h
+
+/-- The `0`-core is the whole group: every group is a `0`-group, since
+`g ^ 0 ^ 1 = g ^ 0 = 1`. -/
+@[simp]
+theorem pCore_zero : pCore 0 G = ⊤ :=
+  pCore_eq_top fun _ => ⟨1, by simp⟩
+
+/-- The `1`-core is trivial: a `1`-group is necessarily the trivial group,
+since `g ^ 1 ^ k = g ^ 1 = g`. -/
+@[simp]
+theorem pCore_one : pCore 1 G = ⊥ := by
+  rw [eq_bot_iff_forall]
+  intro x hx
+  obtain ⟨k, hk⟩ := isPGroup_pCore ⟨x, hx⟩
+  rw [one_pow, pow_one] at hk
+  exact congrArg Subtype.val hk
+
+/-- The `p`-core is contained in every Sylow `p`-subgroup. The argument
+needs no finiteness or primality: `P ⊔ pCore p G` is a `p`-subgroup
+(as the join of a `p`-subgroup with a normal `p`-subgroup), so by
+maximality of `P` it equals `P`. -/
+theorem pCore_le_sylow (P : Sylow p G) : pCore p G ≤ P := by
+  have hpsup : IsPGroup p ((P : Subgroup G) ⊔ pCore p G : Subgroup G) :=
+    P.2.to_sup_of_normal_right isPGroup_pCore
+  have heq : (P : Subgroup G) ⊔ pCore p G = P := P.3 hpsup le_sup_left
+  exact le_sup_right.trans heq.le
+
+/-- The intersection of all Sylow `p`-subgroups is normal: conjugation
+permutes the Sylow `p`-subgroups, so the intersection is fixed. -/
+theorem normal_iInf_sylow : (⨅ P : Sylow p G, (P : Subgroup G)).Normal where
+  conj_mem n hn g := by
+    simp only [mem_iInf] at hn ⊢
+    intro P
+    have h := hn (g⁻¹ • P)
+    rw [Sylow.coe_subgroup_smul, mem_pointwise_smul_iff_inv_smul_mem] at h
+    simpa using h
+
+/-- The intersection of all Sylow `p`-subgroups is a `p`-group, being
+contained in any single Sylow `p`-subgroup. -/
+theorem isPGroup_iInf_sylow : IsPGroup p ↥(⨅ P : Sylow p G, (P : Subgroup G)) :=
+  (Classical.arbitrary (Sylow p G)).2.to_le (iInf_le _ _)
+
+/-- The `p`-core equals the intersection of all Sylow `p`-subgroups.
+This holds for arbitrary groups and arbitrary `p`: each Sylow contains
+`pCore p G` by maximality, and the intersection of Sylows is itself a
+normal `p`-subgroup hence contained in `pCore p G`. -/
+theorem pCore_eq_iInf_sylow : pCore p G = ⨅ P : Sylow p G, (P : Subgroup G) :=
+  le_antisymm (le_iInf pCore_le_sylow) (le_pCore normal_iInf_sylow isPGroup_iInf_sylow)
+
+section Hom
+
+variable {H : Type*} [Group H]
+
+/-- A surjective group homomorphism sends the `p`-core into the `p`-core. -/
+theorem map_pCore_le_pCore {f : G →* H} (hf : Function.Surjective f) :
+    (pCore p G).map f ≤ pCore p H :=
+  le_pCore (pCore_normal.map f hf) (isPGroup_pCore.map f)
+
+/-- A surjective group homomorphism pulls back the `p`-core to a subgroup
+containing the source's `p`-core. (Equivalent to `map_pCore_le_pCore`
+by the `map`/`comap` adjunction.) -/
+theorem pCore_le_comap_pCore {f : G →* H} (hf : Function.Surjective f) :
+    pCore p G ≤ (pCore p H).comap f :=
+  map_le_iff_le_comap.mp (map_pCore_le_pCore hf)
+
+/-- If the kernel of `f : G →* H` is a `p`-group, then the preimage of the
+`p`-core of `H` is contained in the `p`-core of `G`. -/
+theorem comap_pCore_le_pCore {f : G →* H} (hker : IsPGroup p f.ker) :
+    (pCore p H).comap f ≤ pCore p G :=
+  le_pCore (pCore_normal.comap f) (isPGroup_pCore.comap_of_ker_isPGroup f hker)
+
+/-- If `f : G →* H` is surjective with `p`-group kernel, then the `p`-core
+of `G` is the preimage of the `p`-core of `H`. -/
+theorem comap_pCore_eq_pCore {f : G →* H} (hf : Function.Surjective f) (hker : IsPGroup p f.ker) :
+    (pCore p H).comap f = pCore p G :=
+  le_antisymm (comap_pCore_le_pCore hker) (pCore_le_comap_pCore hf)
+
+/-- A group isomorphism preserves the `p`-core. -/
+theorem _root_.MulEquiv.map_pCore (e : G ≃* H) :
+    (pCore p G).map e.toMonoidHom = pCore p H := by
+  rw [map_equiv_eq_comap_symm']
+  exact comap_pCore_eq_pCore e.symm.surjective (IsPGroup.ker_isPGroup_of_injective e.symm.injective)
+
+end Hom
+
+end Subgroup