feat(GroupTheory/MaximalSubgroups): define maximal subgroups

[AntoineChambert-Loir]

---

• depends on: [Merged by Bors] - feat(Order/Atoms): atoms, coatoms in SetLike #20736

[github-actions]

PR summary 6c361461c4

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Order.Atoms	384	386	+2 (+0.52%)

Import changes for all files

Files	Import difference
12 files Mathlib.Order.Partition.Equipartition Mathlib.Data.Finset.Interval Mathlib.Data.Finset.Grade Mathlib.Order.Atoms Mathlib.Order.Radical Mathlib.Data.Setoid.Partition Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.Simple Mathlib.Order.Partition.Finpartition Mathlib.Order.Atoms.Finite Mathlib.Order.KonigLemma	2
Mathlib.GroupTheory.MaximalSubgroups (new file)	420

---

Declarations diff

+ IsMaximal
+ IsMaximal.eq_of_le
+ IsMaximal.eq_top_of_lt
+ IsMaximal.ne_top
+ covBy_iff
+ covBy_iff'
+ isAtom_iff
+ isCoatom_iff
+ isMaximal_def
+ isMaximal_iff

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[alexjbest]

I'm wondering if this would be better off as an abbrev or a def, rather than a one field structure. Did you consider that approach?

[alreadydone]

I'm wondering if this would be better off as an abbrev or a def, rather than a one field structure. Did you consider that approach?

But IsCoatom isn't a class?
This design follows Ideal.IsMaximal.

[alreadydone]

I feel like we should make a SetLike.isMaximal_iff that unifies this and Ideal.isMaximal_iff.

[AntoineChambert-Loir]

That seems to require that the substructure is a sup-lattice.

[alreadydone]

I don't think so? I realized that Ideal.isMaximal_iff differs from this statement by Ideal.eq_top_iff_one, but otherwise OrderTop should be enough.

[alreadydone]

And the proof is pretty easy:

import Mathlib.Data.SetLike.Basic
import Mathlib.Order.Atoms
variable (A B : Type*) [SetLike A B] [OrderTop A]
theorem SetLike.isCoatom_iff {K : A} :
    IsCoatom K ↔ K ≠ ⊤ ∧ ∀ H g, K ≤ H → g ∉ K → g ∈ H → H = ⊤ := by
  simp_rw [IsCoatom, lt_iff_le_not_le, SetLike.not_le_iff_exists,
    and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]

[alreadydone]

I'm wondering if this would be better off as an abbrev or a def, rather than a one field structure. Did you consider that approach?

But IsCoatom isn't a class?
This design follows Ideal.IsMaximal.

[alexjbest]

I was thinking there might be less API / easier to develop the API it it is defeq to the def instead of a 1 field structure

[AntoineChambert-Loir]

As noted by @alreadydone , we just copied the API of maximal ideals. I'm not against doing something else now, but for consistency, it should be done for maximal ideals also, and that's not our purpose here.

[AntoineChambert-Loir]

Actually, given the actual definition, I'm split into two possibilities: the one that we proposed, and the mere omission of maximal ideals, maximal subgroups, etc. to be replaced by people writing IsCoatom, which is precisely what it means. The interest of the former is to be closer to mathematical terminology, the interest of the latter is to refrain from introducing new stuff that will, in turn, require some API.

[AntoineChambert-Loir]

In general, maximal elements could be obtained by Maximal (although it requires an additional predicate), and maximal but not top are just IsCoatom. That would force mathematicians to learn preorder terminology, but would free math from the ambiguity of maximal ideals not being a maximal element of the lattice of ideals.

[faenuccio]

LGTM, thanks.

[faenuccio]

maintainer delegate

[github-actions]

🚀 Pull request has been placed on the maintainer queue by faenuccio.

[ocfnash]

I have the same thought and so I'm not absolutely convinced about the new definition.

However I am convinced that the changes to the files Order/Atoms.lean and Ideal/Maximal.lean are desirable. How would you feel about splitting out a new PR with just those changes for quick merging?

[faenuccio]

@ocfnash I agree that it would be unpleasant to rewrite the same bit of code for all sub-structures. I have the feeling that the path we're taking is to give a new definition for each maximal substructure which is IsCoatom and then we're fearing defeq abuse and we develop a new API instead of relying on that of IsCoatom. Am I wrong?

[ocfnash]

I think you're right. The paths I see are:

1. Add an abbrev for each substructure + write API to reduce temptation for defeq abuse
2. Add an abbrev for each substructure, no API, permit defeq abuse
3. Admit that the abbrev is not really doing anything and just spell all our lemmas using IsCoatom.

IMHO it's subjective but I'd tend toward 3 or maybe 2.

[faenuccio]

Well, I would probably go for 2., telling ourselves that defeq abuse is a problem if the def really contains stuff (so, defeq abuse for IsCoatom is problematic), but it is ok if it is just an abbrev. In a sense, the def at play here is IsCoatom and it is for that one that we should build the API and use that instead of the def. If then something is an abbrev of IsCoatom we will use the API there and that will be helping avoiding defeq abuse. Of course 3. is also OK, but I think that is mathematically pleasant to call a maximal ideal/subgroup as such rather than a "coatomic ideal".

If we all agree (@AntoineChambert-Loir : what's your take on the matter?), shall we start by this PR and simply rely on the IsCoatom API (perhaps explaining in the doc what is going on, possibly pointing to this discussion)?

[tb65536]

The downside of 3 is that then we don't get to use typeclass inference for maximal ideals.

[AntoineChambert-Loir]

I have the same thought and so I'm not absolutely convinced about the new definition.

However I am convinced that the changes to the files Order/Atoms.lean and Ideal/Maximal.lean are desirable. How would you feel about splitting out a new PR with just those changes for quick merging?

I'll do that this afternoon.

[AntoineChambert-Loir]

#20736

[AntoineChambert-Loir]

Regarding the main goal of the PR : It was only used for an alternative characterization of primitive actions (#12052) that involves maximal subgroups. Let me first see if it is possible to formulate this as IsCoatom in that context.

[AntoineChambert-Loir]

Good news: I could remove all explicit mentions of maximal subgroups in #12052, IsCoatom _ worked fine.
That doesn't make this PR absolutely obsolete, but leaves more time to think about what is necessary.
Ultimately, I would like to see formalized theorems of O'Nan-Scott and Aschbacher, Liebeck… that describe the maximal subgroups of Sn, An and geometric groups. But maybe even then, IsCoatom will suffice.

[faenuccio]

After some thought I came to the opinion that perhaps the situation maximal ideal vs maximal subgroup is not really symmetric. To my knowledge, there is a bunch of ancillary notions and constructions associated to that of maximal ideal (localization, residue field, maximal spectrum, etc.) whereas maximal subgroup are "only" CoAtoms among subgroups: certainly there are many results about them but I feel that they fewer things are "built out of them". I am sure @AntoineChambert-Loir will promptly prove me wrong, given his knowledge, but if I happen to be correct I would argue that keeping around the assumption IsCoatom (or simply introducing an abbrev and living with defeq) should be ok, and I would suggest to remove from this PR the boilerplate pertaining to maximal subgroups.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Order/Atoms): atoms, coatoms in SetLike #20736
  By Dependent Issues (🤖). Happy coding!

[AntoineChambert-Loir]

Given that maximal subgroups can be discussed using IsCoatom, and that it suffices for the moment, I suggest that this PR be put on hold, and maybe closed (will it be possible to reopen it if needed?) Le 15 janvier 2025 09:19:05 GMT+01:00, "Filippo A. E. Nuccio" ***@***.***> a écrit :

…

@faenuccio commented on this pull request. > +Will we need to write this for all `sub`-structures ? +In fact, the essentially only justification of this file is `Subgroup.isMaximal_iff`. After some thought I came to the opinion that perhaps the situation _maximal ideal_ vs _maximal subgroup_ is not really symmetric. To my knowledge, there is a bunch of ancillary notions and constructions associated to that of maximal ideal (localization, residue field, maximal spectrum, etc.) whereas maximal subgroup are "only" `CoAtoms` among subgroups: certainly there are many results about them but I feel that they fewer things are "built out of them". I am sure @AntoineChambert-Loir will promptly prove me wrong, given his knowledge, but if I happen to be correct I would argue that keeping around the assumption `IsCoatom` (or simply introducing an `abbrev` and living with `defeq`) should be ok, and I would suggest to remove from this PR the boilerplate pertaining to maximal subgroups. -- Reply to this email directly or view it on GitHub: #20499 (comment) You are receiving this because you were mentioned. Message ID: ***@***.***>

[faenuccio]

Given that maximal subgroups can be discussed using IsCoatom, and that it suffices for the moment, I suggest that this PR be put on hold, and maybe closed (will it be possible to reopen it if needed?)

Yes, it will be possible, so I think you can go ahead and close it.