Dedekind-MacNeille completion.

Stream: maths

[Wrenna Robson]

I thought I'd share this that I was working on today, mostly for fun. I couldn't find the D-McN completion but @Yaël Dillies pointed out that we have it under the name "concept lattice" for general relations.

I assume there's no value in having this twice in mathlib, so I probably shouldn't put it in any kind of PR? Nevertheless i thought I'd ask what people thought of it (to an extent I'm asking for feedback on my code...)

https://github.com/linesthatinterlace/verifying-cmce/blob/main/lean/src/shared/order_theory/dmnc.lean

I will say that there seem like there's a lot of different concepts and names in the order/relation space that are sometimes quite tricky to keep track of, and don't seem to be as connected as they could be. I don't understand why.

[Yaël Dillies]

Unfortunately I think I am the one singular person interested in this :sad:, but maybe @Anne Baanen will have thoughts? (although they're busy right now)

[Wrenna Robson]

Did you see my thoughts elsewhere about using this as a notion to hang the domain of Sup and Inf on? I think it's got some problems and could be done badly but if it works it could I think maybe simplify some stuff

[Wrenna Robson]

Oh also, whether we stick with your concept terminology or use something like my slightly more concrete formulation (the main difference is how we chose to construct the type and you doing it for general relations), it would be good to prove that the reals are isomorphic to this completion of the rationals, although I understand that's only true nonconstructively (or Wikipedia is lying) and in constructive mathematics these objects are much weirder.

[Wrenna Robson]

Do you have that the concept of a concept is isomorphic to itself?

[Antoine Chambert-Loir]

Where does the terminology “concept lattice” come from?

[Wrenna Robson]

As far as I can tell from what Yaël said, one particular book - cited on the page. I've never heard of it before.

[Wrenna Robson]

Indeed that's why I did my own version of the completion - it doesn't mention that's what it is, so my search found nothing, and it isn't the term I was looking for.

[Yaël Dillies]

Well because it's a bit more general as well. You only get Dedekind-MacNeille if you plug in <=.

[Yaël Dillies]

But the truth is that this file is incomplete because my enthusiasm was showered by people here telling me nobody cared about it.

[Yaël Dillies]

I will PR the rest of what I have.

[Wrenna Robson]

https://en.m.wikipedia.org/wiki/Formal_concept_analysis

[Wrenna Robson]

Well, I care about it Yaël, especially if we can use it to tidy up the "sometimes complete" hierarchy.

[Wrenna Robson]

I btw only bundled the one set into the type, and then defined the lower and upper cuts separately - i don't know if that's worse than your way or just different

[Wrenna Robson]

While it is more general, I would argue that sometimes that can make things trickier to use in other contexts, but also if it is possible to do in the generality we should capture the notion that the completion "preserves" certain relations.

[Anne Baanen]

For what it's worth, I think everything in Davey & Priestley is suitable for inclusion in mathlib, since it's used in "serious" maths courses. Since it covers this completion, I'd be happy to see it contributed to mathlib.

[Yaël Dillies]

Let me grab back the book at the library, then!