LowerAdjoint

Stream: mathlib4

[Wrenna Robson]

Why does docs#LowerAdjoint exist in its current form? I'm not saying it shouldn't - it's just I can imagine a world where we have docs#GaloisConnection as a bundled structure, and obviously we have it unbundled, but LowerAdjoint is a semibundled version and this feels to me like a weird design pattern.

[Yaël Dillies]

I personally think we could get rid of it. It was an experiment of mine that went nowhere

[Wrenna Robson]

I don't know if we use ClosureOperator much but that does clearly have some purpose.

[Wrenna Robson]

Why is GaloisConnection unbundled, ooi?

[Wrenna Robson]

Also, I'd be happy to help prepare a PR to get rid of LowerAdjoint - in such a case where a definition is being removed wholesale, how do we add a deprecation notice?

[Yaël Dillies]

See #general > Closure operators @ 💬

[Aaron Liu]

Wrenna Robson said:

Why is GaloisConnection unbundled, ooi?

So you can do stuff like docs#Set.image_preimage without having to bundle them

[Wrenna Robson]

Oh, makes sense.

[Wrenna Robson]

I might expect it to be called IsGaloisConnection but that does make sense.

[Aaron Liu]

We have both docs#Set.image_preimage and docs#Set.preimage_kernImage so it's difficut to have both if it's bundled

[Wrenna Robson]

Yaël Dillies said:

See #general > Closure operators @ 💬

Interesting discussion. Do we define closure operators for, say, topological closure and the like, in the end?