maximals/minimals refactor

Stream: mathlib4

[Peter Nelson]

At the moment Mathlib.Order.Minimal defines maximals r s : Set α and minimals r s : Set α
for r : α → α → Prop and s : Set α. This is awkward to use in the common case where s = SetOf P.

I'd like to refactor things to have a predicate Maximal r P : α → Prop where P : α → Prop instead. This will allow for good API with dot notation, and can be later be used to unify ad hoc expressions of max/minimality in places like LinearIndependent.Maximal and Set.Finite.exists_maximal_wrt.

I wanted to run a couple of questions by people.

• Should the existing maximals and minimals remain as definitions in terms of the new Maximal/Minimal, or should they be replaced entirely by {x | Maximal r (· ∈ s) x} instead?
• Should Maximal r P x instead be Maximal P x with a [Preorder α], as implemented in terms
  of an auxiliary less-used MaximalWrt r P x? Most uses of Maximal are in practice with an existing
  preorder (· ≤ ·); the exception of α = Set β can be easily smoothed over with API.

[Yaël Dillies]

• Probably not
• I think one of my motivations for maximals/minimals was Zorn's lemma, which in mathlib has an unbundled relation version, so it might be nice to not assume Preorder. On the other hand I'm not a huge fan of unbundled preorder relations... I think you could just specialise everything to Preorder without anyone complaining

[Kevin Buzzard]

One motivation for having sets (rather than indexed sets) for bases of vector spaces is that then you can prove every vector space has a basis quite nicely with Zorn's lemma, but every single other use of bases seems to prefer the indexed version. Initially I was in two minds about what a basis should be but now I'm absolutely convinced that Zorn was leading me astray here.

[Peter Nelson]

Yes, sets for bases and linear independence are also a complete no-go for matroid theory. If you have a non-injective function f : α → W for a vector space W, then this gives a matroid in which any two distinct elements in f ⁻¹' {v} form an independent set. It is impossible to express this idea if independence isn't indexed.

[Violeta Hernández]

just weighing in on vector spaces as a mathematician: when we say {v, w} is linearly independent iff v and w are not vector multiples of each other, we're implicitly assuming linear combinations are defined in terms of multisets (or some other indexed structure)

[Violeta Hernández]

Since {v, v} = {v} is linearly independent as a set if v ≠ 0

[Peter Nelson]

Yup. It’s certainly a technicality that we carefully avoid talking about when teaching linear algebra.

[Johan Commelin]

I was taught linear algebra by Lenny Taelman who did point these things out to us (-;

[Peter Nelson]

#14721. Also see the PR review thread.

Reviews appreciated!