Maximal subgroups #20499

Stream: PR reviews

[Antoine Chambert-Loir]

In #20499, @María Inés de Frutos Fernández and I formalize maximal subgroups of a group, by merely copying what is done for maximal ideals in docs#Ideal.IsMaximal, but encapsulating the notion in a one-field structure that says IsCoatom K.

In the review process, the issue was raised of whether we shouldn't simply use an abbrev to IsCoatom K. But then, maximal ideals should be phrased in the same way.
And maybe mathlib users should just learn about docs#IsCoatom and use it instead of the mathematically more idiomatic (but also more ambiguous, since maximal ideals are not maximal elements of the lattice of ideals) terminology.

[Yakov Pechersky]

Thing about ideals is that there, the class aspect is used for theorems that take the IsMaximal hypothesis as a TC argument

[Yakov Pechersky]

While IsCoatom is not a class, so one can't do the same

[Yakov Pechersky]

In particular, I believe the IsMaximal for ideals is set up this way so that a quotient by an ideal can be synthesized by TC inference to be a Field, in the appropriate situation

[Johan Commelin]

I do agree that maximal ideals could be refactored to use IsCoatom. The current situation is a historical artifact: maximal ideals in mathlib are older than IsCoatom.

[Johan Commelin]

The point about IsMaximal being a class in order to get a field instance on the quotient is valid. And I don't think a similar argument applies to maximal subgroups. So it is probably easier to work directly with IsCoatom there.

[Johan Commelin]

@Thomas Browning Do you have thoughts on this?

[Thomas Browning]

Yes, those are basically my thoughts. I can't immediately think of a situation where typeclass inference would be helpful for working with maximal subgroups, although I can't rule it out.

[Andrew Yang]

Ideal.IsMaximal is already defined as

class IsMaximal (I : Ideal α) : Prop where
  out : IsCoatom I

[Johan Commelin]

Thanks for pointing that out (-;

[Edward van de Meent]

pointing that out :looking:

[Matthew Ballard]

That seems like an easy rename for the field.