[Merged by Bors] - feat(order): closure operators

[b-mehta]

Adds closure operators on a partial order, as in wikipedia. I made them bundled for no particular reason, I don't mind unbundling.

[kbuzzard]

Looks great! Is there a Galois insertion one can prove here?

[b-mehta]

Added the Galois insertion!

[urkud]

There are two kinds of closure operators in mathlib now:

• in topology, we use closure : set α → set α;
• in submonoids, submodules etc, we use submonoid.closure : set M → submonoid M.

How hard is it to have a general theory that works in both settings? Something like closure_operator {α β : Type*} (f : β → α) + 2 notations/abbreviations for closure_operator α α (λ x, x) and closure_operator α β coe?

[b-mehta]

There are two kinds of closure operators in mathlib now:

• in topology, we use closure : set α → set α;
• in submonoids, submodules etc, we use submonoid.closure : set M → submonoid M.

How hard is it to have a general theory that works in both settings? Something like closure_operator {α β : Type*} (f : β → α) + 2 notations/abbreviations for closure_operator α α (λ x, x) and closure_operator α β coe?

I'm not sure how your suggestion would work - to state idempotency and extensivity the domain and range of the operator need to be the same. The obvious fix here is to include the reverse as well, but then the notion is exactly a Galois insertion, which I think is the general theory you're looking for. Should I make it more clear in this file that closure operators are just special cases of Galois insertions?

[bryangingechen]

Could you mention the connection to Galois insertions in the module docstring?

[bryangingechen]

LGTM, but I'll let @urkud take a look.

[eric-wieser]

Are there any functions already in mathlib than can be bundled in this way?

[b-mehta]

Perhaps closure : set α → set α for topologies as Yury mentioned could be done - I'd expect there could be more but I'm not certain. That said, my guess is that in practice when the closure operator is fixed and has an explicit definition, it's more helpful to express as a Galois insertion with the subtype of closed elements rather than as an endomorphism like this. I think the main use case for this file is for general closure operators (eg Moore collections, universal closure operators). In any case, I think explicit examples can happen in another PR :)

[bryangingechen]

Let's merge this now, but I do want to see some (more) examples in future PRs.

Thanks!
bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests