feat(GroupTheory/PCore): define the p-core of a group#39771
Draft
kim-em wants to merge 10 commits into
Draft
Conversation
PR summary 9a62cc0831Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
Comment on lines
+57
to
+58
| def pCore (p : ℕ) (G : Type*) [Group G] : Subgroup G := | ||
| ⨆ N : {N : Subgroup G // N.Normal ∧ IsPGroup p N}, (N : Subgroup G) |
Collaborator
There was a problem hiding this comment.
What's the advantage of this over the intersection of all Sylow-p Subgroups?
Contributor
Author
There was a problem hiding this comment.
Both definitions agree unconditionally. I had this wrong before, but I've dropped [Fact p.Prime] [Finite G] from pCore_eq_iInf_sylow. I think the iSup definition gives the universal-property and hom-behaviour lemmas more directly.
This PR adds `Subgroup.pCore p G`, the largest normal `p`-subgroup of `G`, classically denoted `O_p(G)`. Defined as the supremum of all normal `p`-subgroups; proved to be itself a normal `p`-group, without any finiteness hypothesis on `G`. The proof that `pCore p G` is a `p`-group uses the fact that the family of normal `p`-subgroups is directed under `≤` (the join of two normal `p`-subgroups is again a normal `p`-subgroup, by the existing `Subgroup.sup_normal` and `IsPGroup.to_sup_of_normal_left`), so `mem_iSup_of_directed` gives: every element of the supremum lies in one of the summands, and therefore has `p`-power order. Used downstream in `leanprover/lean-eval` to state the Baer-Suzuki theorem (leanprover/lean-eval#311). Follow-up work (filed in module TODO): * `pCore p G = ⨅ P : Sylow p G, (P : Subgroup G)` for finite `G` and prime `p`. * Behaviour of `pCore` under group homomorphisms. * Interaction with `IsSolvable`.
For a finite group `G` and a prime `p`, the `p`-core equals the intersection of all Sylow `p`-subgroups: `pCore p G = ⨅ P : Sylow p G, (P : Subgroup G)` New lemmas: * `Subgroup.pCore_le_sylow` — `pCore p G` is contained in every Sylow `p`-subgroup (uses that `pCore` is a normal `p`-subgroup so equals its conjugate, plus Sylow conjugacy). * `Subgroup.normal_iInf_sylow` — the intersection of all Sylow `p`-subgroups is normal (conjugation permutes Sylows). * `Subgroup.isPGroup_iInf_sylow` — the intersection is a `p`-group (contained in any one Sylow). * `Subgroup.pCore_eq_iInf_sylow` — the main result. Changes the import from `PGroup` to `Sylow` to access Sylow theory. Proof contributed via Codex pair-programming.
Cleanup pass: * Extract `Nonempty` subtype instance to top-level (was duplicated as `haveI` in `isPGroup_pCore` and `mem_pCore_iff`). * Replace `@`-instance threading in `directed_normal_isPGroup` with `haveI`-based instance synthesis. * Collapse the `1` case in `pCore_normal` to `by simp`. * Simplify the final `Subtype.ext` in `isPGroup_pCore` to `ext + simpa`. * Unify the two branches in `normal_iInf_sylow` to a single direction (one-sided argument suffices via `mem_pointwise_smul_iff_inv_smul_mem`). * Drop unnecessary `classical` calls and `MulAut.conj_apply` hint. * Replace `(isPGroup_pCore (G := G) (p := p))` with a clean `have hpg : IsPGroup p (pCore p G) := isPGroup_pCore` step. * Switch `normal_iInf_sylow` from `refine ⟨...⟩` to `where conj_mem` to match the style used by `pCore_normal`.
Codex review pass: * Add `Subgroup.normal_iSup_normal` to `Pointwise.lean` (sibling of the existing `normal_iInf_normal` in `Basic.lean`; needed `iSup_induction` which lives in `Pointwise.lean`). Generalizes the supremum-of-normals-is-normal proof previously inlined in `pCore_normal`. * Simplify `pCore_normal` to a one-liner using the new general lemma. * Add `pCore_eq_bot_iff` (the `p`-core is trivial iff `G` has no non-trivial normal `p`-subgroup). * Add `pCore_eq_top` (if `G` is itself a `p`-group, the `p`-core is the whole group). * Rename module-doc "Notation" section to "Terminology" (the section describes the textbook name `O_p(G)`, but introduces no notation). Kept `directed_normal_isPGroup` public (per user preference): it is genuinely useful API for anyone working with `pCore`, not just a private implementation lemma. The `to_additive` translation of `normal_iSup_normal` is left for a follow-up; the multiplicative proof routes through `MulAut.conj`, which translates but its `map_mul` step needs a small workaround in the additive setting.
Mirrors the API for `Subgroup.normalCore`: * `normal_le_pCore` — for `N` normal in `G`, `N ≤ pCore p G ↔ IsPGroup p N`. Previously only the (←) direction was available (`le_pCore`). * `pCore_eq_top_iff` — `pCore p G = ⊤ ↔ IsPGroup p (⊤ : Subgroup G)`. Previously only the (←) direction (`pCore_eq_top`); the (→) direction follows from `isPGroup_pCore.to_le`.
For a homomorphism `f : G →* H`: * `map_pCore_le_pCore (hf : Surjective f)`: `(pCore p G).map f ≤ pCore p H` — the image of the `p`-core under a surjective hom is a normal `p`-subgroup of `H`, hence in its `p`-core. * `pCore_le_comap_pCore (hf : Surjective f)`: the same fact restated via the map-comap adjunction. * `comap_pCore_le_pCore (hker : IsPGroup p f.ker)`: when the kernel is a `p`-group, the preimage of `pCore p H` is a normal `p`-subgroup of `G`, hence in `pCore p G`. * `comap_pCore_eq_pCore (hf : Surjective f) (hker : IsPGroup p f.ker)`: both conditions together give equality. * `MulEquiv.map_pCore`: a group isomorphism preserves the `p`-core (immediate from the equality above with `e.symm`). These cover the classical hom-behaviour story for `O_p(G)`. Removes the "Behaviour of `pCore` under group homomorphisms" item from the module TODO.
…pCore Shorter, more idiomatic name tied to the pCore definition.
The original proof used `MulAut.conj g` and `map_mul`. The `to_additive` translation of `MulAut.conj` is `AddAut.conj`, whose codomain is `Additive (AddAut G)` (wrapping the inherently multiplicative automorphism group), so the proof did not translate. Replace with the same `simp only [mul_assoc, inv_mul_cancel_left]` manipulation that the existing `sup_normal` (immediately above) uses for the analogous step. Both `mul_assoc` and `inv_mul_cancel_left` have `@[to_additive]`, so the proof now translates cleanly. The lemma `AddSubgroup.normal_iSup_normal` is now also exported and mirrors the existing `AddSubgroup.normal_iInf_normal` in `Basic.lean`.
…lignment The Sylow alignment `pCore p G = ⨅ P : Sylow p G, (P : Subgroup G)` is unconditional, not specific to finite groups or prime `p`: * `pCore_le_sylow` (no longer needs `[Fact p.Prime] [Finite G]`): for any Sylow `P`, the join `P ⊔ pCore p G` is a `p`-subgroup (by `IsPGroup.to_sup_of_normal_right`), so maximality of `P` forces `P ⊔ pCore = P`, hence `pCore ≤ P`. * `normal_iInf_sylow` (no hypotheses): conjugation permutes the Sylows, so the intersection is invariant. * `isPGroup_iInf_sylow` (no hypotheses): the intersection lies in any one Sylow, hence is a `p`-group. `Sylow.nonempty` is unconditional. * `pCore_eq_iInf_sylow` (no hypotheses): le_antisymm of the above. The new proof of `pCore_le_sylow` is also shorter — it avoids the Sylow-II conjugacy machinery (`MulAction.exists_smul_eq`) entirely.
Edge cases: * `pCore_zero`: `pCore 0 G = ⊤`. Every group is a `0`-group via `g ^ 0 ^ 1 = g ^ 0 = 1`. * `pCore_one`: `pCore 1 G = ⊥`. A `1`-group must be trivial, since `g ^ 1 ^ k = g ^ 1 = g`. Both marked `@[simp]`.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds
Subgroup.pCore p G, the largest normalp-subgroup ofG, classically denotedO_p(G).Defined as the supremum of all normal
p-subgroups; proved to be itself a normalp-group, without any finiteness hypothesis onGor primality ofp.The proof that
pCore p Gis ap-group uses the fact that the family of normalp-subgroups is directed under≤(the join of two normalp-subgroups is again a normalp-subgroup, by the existingSubgroup.sup_normalandIsPGroup.to_sup_of_normal_left), somem_iSup_of_directedgives: every element of the supremum lies in one of the summands, and therefore hasp-power order.Core properties:
Subgroup.pCore,Subgroup.pCore_normal(instance),Subgroup.isPGroup_pCore,Subgroup.le_pCore,Subgroup.normal_le_pCore(iff version forNnormal),Subgroup.mem_pCore_iff,Subgroup.pCore_eq_bot_iff,Subgroup.pCore_eq_top_iff/pCore_eq_top.Sylow alignment (unconditional — also for non-prime
pand infiniteG):Subgroup.pCore_le_sylow(pCore p Gis contained in every Sylow, by the normal-join argument with maximality),Subgroup.normal_iInf_sylow,Subgroup.isPGroup_iInf_sylow,Subgroup.pCore_eq_iInf_sylow—pCore p G = ⨅ P : Sylow p G, (P : Subgroup G).Homomorphism behaviour for
f : G →* H:Subgroup.map_pCore_le_pCore(surjectivef),Subgroup.pCore_le_comap_pCore(same fact via themap/comapadjunction),Subgroup.comap_pCore_le_pCore(whenf.keris ap-group),Subgroup.comap_pCore_eq_pCore(both conditions give equality),MulEquiv.map_pCore(isomorphism case).Also added
Subgroup.normal_iSup_normalinMathlib/Algebra/Group/Subgroup/Pointwise.lean: the supremum of a family of normal subgroups is normal. Marked@[to_additive], soAddSubgroup.normal_iSup_normalis also generated. This is the sibling of the existingnormal_iInf_normalinSubgroup/Basic.lean.Used downstream in leanprover/lean-eval#311 to state the Baer-Suzuki theorem.
🤖 Prepared with Claude Code