proposal: lattice operations on `SetLike`s?

Stream: mathlib4

[David Loeffler]

Mathlib has a lot of types for "sub-Foos of a Foo" – e.g. subgroups, submonoids, subrings, etc – which all use the SetLike typeclass to record that they coerce to subsets of the parent.

In many cases these sub-Foo types have lattice or semilattice structures (sup, inf, top, bottom, etc), which are frequently, but not always, compatible with coercion to Set; e.g. for subgroups of a group, inf is intersection, but sup is something else (the subgroup generated by the two given subgroups). The API for these is defined separately in each case, leading to a great deal of duplicated code.

I think this could be factored out by using typeclasses asserting "this SetLike class has an inf compatible with set intersection", something like

class LawfulInf (α X : Type*) [SetLike α X] extends Min α where
  coe_inf' {a b : α} : (↑(a ⊓ b) : Set X) = ↑a ∩ ↑b

and similarly for top, bot, sInf, etc. Then we can develop all the API once for an arbitrary SetLike satisfying the appropriate LawfulXXX typeclasses, rather than proving lemmas like mem_inf etc over and over again.

What's the opinion of the community on this? Would this be a worthwhile refactor? This would be quite a lot of work to implement, so I wanted to ask for opinions here first.

[Jireh Loreaux]

Isn't there a recent thread involving @Johan Commelin and @Yaël Dillies (among others) about this?

[Jireh Loreaux]

I thought the consensus there was to stop creating the LE instance from SetLike directly.

[Yaël Dillies]

cc @Artie Khovanov

[Patrick Massot]

#mathlib4 > Abstracting out .closure, .adjoin

[Artie Khovanov]

Great minds think alike :p
@David Loeffler see my proposal in progress at #20621

[Artie Khovanov]

Note that "LawfulSInf" is pretty much always true and implies "LawfulTop", "LawfulInf", and the existence of a CompleteLattice structure
OTOH "LawfulSSup", "LawfulSup", "LawfulBot" are pretty much always false, and when they're true it's for a "genuinely mathematical" reason, rather than just the fact that these substructures are given by a single carrier field and then a bunch of closure conditions.
So I've just gone with the one typeclass for simplicity.

[David Loeffler]

"LawfulSSup", "LawfulSup", "LawfulBot" are pretty much always false

LawfulSup and LawfulBot are true for some interesting SetLikes, e.g. open sets in a topological space. But these aren't really of the nature of "subFoo's of a Foo".

[Artie Khovanov]

Indeed. Obviously you could also build out those abstractions, but I'm not sure how much they would be reused.

[David Loeffler]

Artie Khovanov said:

Great minds think alike :p
David Loeffler see my proposal in progress at #20621

"Files changed: 154" - ouch!

[Artie Khovanov]

Those changes are mostly from the PR it depends on (#20638)
In my draft, I've only done the full refactor for one substructure -- the simplest (Subsemigroup) -- as a proof of concept. When completed, this refactor will change hundreds of files, mostly to rename usages of previously-duplicated theorems.

[David Loeffler]

Just out of interest, can you prove a version of docs#Subsemigroup.mem_iSup_of_directed for a LatticeSetLike?

[Artie Khovanov]

Yes, I should be able to -- after all, the infima determine the suprema.
Let me try now.

[David Loeffler]

I think it needs more axioms than you currently have: I think it's false for closed subspaces of topological vector spaces (which are preserved by arbitrary intersections, but not by filtered unions).

[Artie Khovanov]

As yep, the missing axiom is basically the conclusion of mem_iSup_of_directed
It says that the embedding into the power set reflects directed unions

[Artie Khovanov]

Proving this is a bit different each time (you might need to induct on different closure axioms), but the consequences are always the same. I think abstracting it out is outside of the scope of my current refactor, but of course you or anyone else is very welcome to have a go!

[Johan Commelin]

It's funny that so many people have come to this conclusion at roughly the same time.

[Johan Commelin]

May I suggest that we merge the two threads of discussion, going forward?
Let's continue with #mathlib4 > Abstracting the substructure lattice construction, since that thread is slightly older.