Commit 2024-08-05 16:52 124f27e8

refactor(Order/Minimal): change minimality to a predicate (#14721) This PR changes the notion of minimality from being a set with an unbundled relation r (i.e. having type signature minimals (r : α → α → Prop) (s : Set α) : Set α) to being a predicate with a bundled order relation in a typeclass: Minimal [LE α] (P : α → Prop) : α → Prop. It also does the same for maximality. This is hopefully an improvement, for a few reasons :

• ergonomic API with dot notation (eg Minimal.eq_of_le, Minimal.not_lt),
• no need to specify a particular relation explicitly (no use of minimals/maximals for a relation that was not defeq to LE.le currently appears anywhere in mathlib),
• the potential in future to unify ad hoc notions of min/maximality appearing in various locations in mathlib (eg zorn_preorder, Sylow.is_maximal' to name a couple of random examples). Since this change removes the definitions minimals and maximals and all their API, it required a total overhaul of the contents of Order.Minimal, and necessarily required updating all uses of maximals/minimals elsewhere. There were not all too many of these; this PR is designed to be the smallest it could be while making this change. The changes required outside Order.Minimal were:

• redefinition of Ideal.minimalPrimes in RingTheory/Ideal/MinimalPrime to use Minimal rather than minimals, with the necessary minor changes to proofs that used the old definition, including in AlgebraicGeometry/PrimeSpectrum/Basic.
• redefinition of irreducibleComponents in Topology/Irreducible to use Minimal rather than minimals, with necessary minor changes to proofs that used the old definition.
• updating of the maximality used in the definition of a matroid in Data/Matroid/Basic from maximals to Maximal, with the necessary changes to everywhere in Data/Matroid/* that a matroid was specified using the definition directly.
• the necessary changes to two lemmas in Data/Finset/Lattice that used minimals/maximals in the statements. I attempted to clean up the API in Order.Minimal to work smoothly with the new definitions, but numerous judgment calls were needed; I removed a few lemmas about maximals/minimals that were used nowhere, and seemed unlikely to be useful with the new definition. Comment is welcome!