Dedekind-MacNeille completion

Stream: maths

[Violeta Hernández]

Has there been any progress on this?

[Violeta Hernández]

@Wrenna Robson Is it ok if I adapt your code for Mathlib 4 and PR it?

[Wrenna Robson]

Crack on, I'm not going to. Let me know and I'll have a look at the PR though.

[Wrenna Robson]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Concept.html

[Wrenna Robson]

I think this is the rest of the Concept stuff, which iirc this basically is.

[Wrenna Robson]

(So you may not want to entirely duplicate it.)

[Wrenna Robson]

@Yaël Dillies what exactly did you end up doing with this?

[Wrenna Robson]

It looks to me like we are missing 3.7-3.9 from Davey & Priestley

[Wrenna Robson]

#general > conditional lattice refactor

@Violeta Hernández you may want to see this thread if you haven't already which was from a little later in 2022.

[Violeta Hernández]

Wrenna Robson said:

I think this is the rest of the Concept stuff, which iirc this basically is.

Oh oops. Would've done me good to read this two hours ago.

[Wrenna Robson]

;_;

[Wrenna Robson]

sorry, I realised it as soon as I got into work

[Wrenna Robson]

there is still work to do (which I am now noodling at...)

[Wrenna Robson]

I'm refactoring Yael's work somewhat to taste and aiming for the fundamental theorem. Then we just need the <= special case :)

[Violeta Hernández]

So, just to make sure I understand, the Dedekind-MacNeille completion is just the concept lattice of the ≤ relation of an order?

[Wrenna Robson]

Yes.

[Violeta Hernández]

huh

[Wrenna Robson]

Which stated kind of another way, is: any complete lattice is the concept lattice of ≤ (so all complete lattices are isomorphic to a concept lattice).

[Violeta Hernández]

What does the fundamental theorem of concept lattices say?

[Violeta Hernández]

My PR had a proof that every embedding into a complete lattice factored through the Dedekind completion; does that have a concept lattice analog?

[Wrenna Robson]

Yes: "The concepts of a given context form a complete lattice into which the original objects and attributes embed."

[Violeta Hernández]

Well, what I'm saying is a bit stronger, isn't it? The Dedekind completion of α is a complete lattice β with an order embedding α ↪o β, but it also has the property that for any other complete lattice γ with an embedding α ↪o γ, you can construct the embedding β ↪o γ such that the triangle commutes.

[Wrenna Robson]

I think this does have an analogue but I'm not yet sure we have it in the Concept stuff (which is certainly incomplete), and it might not be in the book.

[Violeta Hernández]

(I'm trying to read up on concept theory, but the Wikipedia article is genuinely incomprehensible...)

[Wrenna Robson]

see your DMs :)

[Violeta Hernández]

I feel like at the very least we should add some sort of docstring somewhere in the file containing the substring "Dedekind-MacNeille".

[Wrenna Robson]

Yes.

[Wrenna Robson]

I don't think it would be BAD to have a separate file which essentially contains the Dedekind-MacNeille completion, even if it's ultimately defined in terms of concepts.

[Violeta Hernández]

Maybe we can define DedekindCut α as an abbreviation for Concept α α (· ≤ ·), and add the theorems linking the intent/extent closure to the lower/upper bounds of a set?

[Wrenna Robson]

Yes, though they are near immediate:

theorem upperBounds_eq_upperPolar [LE α] : upperBounds s = upperPolar (· ≤ ·) s := rfl
theorem lowerBounds_eq_lowerPolar [LE β] : lowerBounds t = lowerPolar (· ≤ ·) t := rfl

(I've renamed the closures but you can see the point.)

[Violeta Hernández]

Hmm, that's a bit too immediate for my taste if I'm being honest

[Violeta Hernández]

Maybe we can add the abbreviation and keep it at that?

[Wrenna Robson]

In what sense?

[Wrenna Robson]

Oh as in it is Just There

[Wrenna Robson]

yes, I did think this.

[Wrenna Robson]

I am going to keep noodling at this refactor and extension for enrichment, thanks for reminding me of it, I'll let you know when I have something. I think we're both keen to get this in in some form.

[Violeta Hernández]

Violeta Hernández said:

Maybe we can add the abbreviation and keep it at that?

Actually, on second thought. What do you think about having a file that defines the abbreviation, but also proves the minimality theorem I mentioned?

[Wrenna Robson]

I think that would be great (though the minimality theorem might apply for concepts in which case we should have it).

[Wrenna Robson]

But basically I think we should have a file that requires people to know NOTHING about concepts that gives the Dedekind-MacNeille completion.

[Wrenna Robson]

Even if, ohoho, it is a simple thin layer over a different file that is the Concept one.

[Violeta Hernández]

@Wrenna Robson Opened a new PR defining DedekindCut α = Concept α α (· ≤ ·). I'm pleasantly surprised at how little work it took to port the minimality theorem.

#26966

[Wrenna Robson]

Oh very nice

[Violeta Hernández]

I imagine we also want to show the Dedekind completion of a complete lattice is isomorphic to itself, surely this theorem doesn't have a concept analog either?

[Wrenna Robson]

Uh that is sort of one end of the fundamental theorem.

[Violeta Hernández]

Oh, nice!

[Violeta Hernández]

Then it's a good thing I haven't done that yet

[Violeta Hernández]

I'll go read the paper you sent me

[Wrenna Robson]

Like in the sense that any complete lattice is isomorphic to the concept lattice of its <=, which IS the completion, essentially.

[Violeta Hernández]

Hmm... I mean, surely we can just state this in terms of DedekindCut?

[Wrenna Robson]

Quite probably!

[Wrenna Robson]

Certainly I think it's a good reason to have DedekindCut as a name.

[Violeta Hernández]

DedekindCut.ofElement would provide one half of the isomorphism, the other half should simply be sSup x.fst

[Wrenna Robson]

That sounds right to me!

[Wrenna Robson]

It's a really neat construction really.

[Wrenna Robson]

I am gonna finish what I am doing I think, but it's alright, I'm sure we can bring it all together.

[Violeta Hernández]

Just finished the proof! Put it in my own branch: https://github.com/vihdzp/mathlib4/blob/vi.ddk2/Mathlib/Order/Dedekind.lean

[Wrenna Robson]

Oh that's quite lovely :)

[Violeta Hernández]

Not sure if I should add this to my original PR, or if I should put this as a separate PR. What do you think?

[Wrenna Robson]

Hmm.

[Wrenna Robson]

Probably a separate dependent PR? Your first should ideally be as close to just adding the abbrev as possible I think (so possibly the factor theorem goes in the second one too).

[Violeta Hernández]

I'm not sure if I agree with that. The point of doing the factor theorem together with the abbrev is that it serves as battle-testing; specifically, it shows you don't have to go through any complicated Concept API to work with DedekindCut.

[Yaël Dillies]

Wrenna Robson said:

Yaël Dillies what exactly did you end up doing with this?

Everything I did is in mathlib

[Wrenna Robson]

Cool :)

[Yaël Dillies]

Note that somewhat recently @Laurent Bartholdi accidentally duplicated part of the concept file in Order.Rel.GaloisConnection. I reviewed his PR but failed to spot that it was a duplicate. If you are cleaning things up, then you could look at removing (most of) Order.Rel.GaloisConnection

[Yaël Dillies]

Violeta Hernández said:

Wrenna Robson said:

I think this is the rest of the Concept stuff, which iirc this basically is.

Oh oops. Would've done me good to read this two hours ago.

Please add "Dedekind-MacNeille completion" in the tags of Order.Concept so as to minimise the likelihood that this happens again

[Wrenna Robson]

Oops.

[Violeta Hernández]

Wrenna Robson said:

Probably a separate dependent PR? Your first should ideally be as close to just adding the abbrev as possible I think (so possibly the factor theorem goes in the second one too).

The way I see it, the factor theorem is proving that the definition of DedekindCut as a concept lattice is correct.

[Violeta Hernández]

I could just add the alias and the upperBounds_fst/lowerBounds_snd theorems, but then the PR would be five lines long and not very interesting.

[Wrenna Robson]

Hmm. I gotta dash to lunch and then I have a meeting but I will try to think more later.

[Wrenna Robson]

Is it just the one branch you have?

[Violeta Hernández]

The other branch is the one in the PR

[Wrenna Robson]

Right right

[Violeta Hernández]

I actually made a second PR, but that's just a few results on Concept itself I felt were missing

[Wrenna Robson]

Hmm, what is the definition of join-dense and meet-dense in Lean?

[Violeta Hernández]

I don't know. What is their definition in general? :sweat_smile:

[Wrenna Robson]

"a subset Q of an ordered set P is called join-
dense if every element of P is the join of a subset of Q."

[Violeta Hernández]

Haven't seen something like that

[Wrenna Robson]

Basically looking at this:
3.8 Theorem. Let (G, M, I) be a context and L = B(G, M, I) the
associated complete lattice of concepts. Then the mappings γ : G → L
and μ : M → L are such that the set γ(G) is join-dense in L,the set
μ(M ) is meet-dense in L,and gIm is equivalent to γ(g) <= μ(m) for
each g ∈ G and m ∈ M .

[Violeta Hernández]

Unless we have yet another tagging situation I don't think join-dense or meet-dense sets are in Mathlib

[Wrenna Robson]

Hmm!

[Violeta Hernández]

Are there any interesting results about them we could formalize?

[Wrenna Robson]

I think elsewhere in the same textbook the concepts are in, but in chapter 2. It would definitely be good to look at formalising them (possibly not in the same way the textbook does, as ever).

[Wrenna Robson]

https://github.com/linesthatinterlace/mathlib4/tree/concept_work

[Wrenna Robson]

So this is the branch I've been working on

[Wrenna Robson]

Bit different to yours!

[Wrenna Robson]

rel_iff_ofObject_le_ofAttribute is interesting to look at!

[Wrenna Robson]

I've been refactoring the existing file to make the API a bit better in terms of names etc.

[Violeta Hernández]

Are lowerPolar and upperPolar the names in the literature?

[Wrenna Robson]

They appear to be, or rather they are called "polars"

[Wrenna Robson]

And given lowerPolar is lowerBounds in the special case of <=, etc., that is why I chose those names.

[Wrenna Robson]

Similarly, "extent" and "intent" come from the literature.

[Violeta Hernández]

I like what you've done!

[Wrenna Robson]

Thanks! It would be good to work with you and bring our stuff together.

[Violeta Hernández]

I notice that ofObject and ofAttribute seem to be the generalizations of my single ofElement map

[Wrenna Robson]

That is correct.

[Violeta Hernández]

I can put my PR on draft. In a weird twist of events it turns out I don't even need it anymore!

[Wrenna Robson]

Isn't that always the way!

[Violeta Hernández]

(I wanted to define gaps of surreal numbers as Concept _ _ (· ≤ ·), but oddly enough it turns out the correct definition is Concept _ _ (· < ·) which is slightly different)

[Wrenna Robson]

But I will have time on and off to work on this and I think we could make some improvements by incorporating what I've done and then layering on top and around the DedkindCut stuff you've done, and the corresponding results.

[Wrenna Robson]

Aha! Good to have the concept language, isn't it?

[Violeta Hernández]

Truly is!

[Wrenna Robson]

There is an argument that you could define the set of sets which are IsExtent/IIsIntent (invariant under lowerPolar r (upperPolar r s) = s and vice vera`), as in give them a name, and then essentially both of those set of sets has a complete lattice structure on it that is isomorphic to the concept lattice.

[Aaron Liu]

This is similar happening with docs#LowerSet and docs#UpperSet right now and I don't like it (which one do I use?)

[Wrenna Robson]

(Notably the joins/meets are not quite the same as the ambient ones from Set - there is an interesting subtlety.)

[Violeta Hernández]

I opened #26968 with some results that are still useful for talking about surreal gaps. I've drafted the Dedekind cut PR in anticipation for the concept API to expand a bit first.

[Wrenna Robson]

LowerSet is different I think - lowerPolar is analgous to lowerBounds instead.

[Wrenna Robson]

Aaron Liu said:

This is similar happening with docs#LowerSet and docs#UpperSet right now and I don't like it (which one do I use?)

Ah but my putative thing above would be the corresponding thing... yeah.

[Wrenna Robson]

It's difficult because basically LowerSet is only special because it has <= associated with it.

[Wrenna Robson]

But that's just some particular relation.

[Violeta Hernández]

Wrenna Robson said:

There is an argument that you could define the set of sets which are IsExtent/IIsIntent (invariant under lowerPolar r (upperPolar r s) = s and vice vera`), as in give them a name, and then essentially both of those set of sets has a complete lattice structure on it that is isomorphic to the concept lattice.

I prefer defining both at once. Lower sets and upper sets often appear on their own, but surely intents and extents are something you only ever talk about together.

[Wrenna Robson]

I don't disagree, which ultimately is why Concept is right I think.

[Wrenna Robson]

It has a good symmetry to it.

[Wrenna Robson]

Right I gotta go home for now and then I will try not to fall down a concept hole tomorrow (but thanks Violeta for pushing me down one ;))

[Violeta Hernández]

Wrenna Robson said:

It has a good symmetry to it.

It also leads to better def-eqs!

[Wrenna Robson]

Yes!

[Wrenna Robson]

Basically the funny thing is that you generally have two choices of "correct" ext/injection style lemma in a proof - some constructions will want to use the extent and some will want to use the intent, and you need to move between them.

[Wrenna Robson]

That's why good API is really important here I think.

[Violeta Hernández]

I think it'd be nice to get the intentClosure → lowerPolar rename done quickly, or we'll end up with more and more theorems to rename.

[Wrenna Robson]

Agreed. Possibly the thing there is a rename PR that doesn't change anything else

[Wrenna Robson]

I.e. no new defs or theorems

[Violeta Hernández]

Agreed

[Violeta Hernández]

I can get that done rn if you want :slight_smile:

[Violeta Hernández]

Opened #26976 for the rename

[Wrenna Robson]

Thanks, sorry I'm still commuting home

[Aaron Liu]

I feel like extends Set α × Set β is really weird, it gives a Concept.toProd projection

[Violeta Hernández]

No worries!

[Wrenna Robson]

Yes I agree, I think we should also get rid of that as in my branch above. Think we could do that in the rename one

[Violeta Hernández]

I don't really see the issue, this projection is basically invisible.

[Wrenna Robson]

Basically I would rather have initialize_simps_projections Concept (fst -> extent, snd -> intent).

[Violeta Hernández]

Oh wait you're right, we can in fact choose better names for these fields

[Wrenna Robson]

I'm not sure the intent closure is what you say it is in the PR. I guess that's as good a name as any though.

[Wrenna Robson]

Yeah, look in my branch to see what I do :)

[Violeta Hernández]

The intent closure is just the smallest intent containing a set, isn't it?

[Violeta Hernández]

Wikipedia says as much

[Wrenna Robson]

Ah, yes.

[Wrenna Robson]

Yes indeed.

[Wrenna Robson]

Sorry, train maths.

[Wrenna Robson]

So that's another thing we should probably define.

[Violeta Hernández]

I don't think it needs a definition. Writing lowerPolar r (upperPolar r s) is straightforward enough.

[Wrenna Robson]

Yeah I don't disagree.

[Violeta Hernández]

We could add a theorem stating IsIntent t → s ⊆ t → lowerPolar r (upperPolar r s) ⊆ t. Can't be very dificult to prove.

[Wrenna Robson]

No that must be pretty obvious. But not in this PR!

[Wrenna Robson]

I would be happy with a notation for it by the way.

[Wrenna Robson]

But I can't think of one.

[Violeta Hernández]

It'd be nice if we could use A' notation, but I suspect the inherent ambiguity won't let us

[Violeta Hernández]

By the way, do I do the fst → intent rename in the intentClosure → lowerPolar PR? Or do I make a separate one?

[Violeta Hernández]

I feel like there's a case for both options

[Wrenna Robson]

Yeah, you need to specify the relation. And that's sufficient, technically, because you could instead of lowerPolar and upperPolar use swap r

[Wrenna Robson]

I think do that in the same PR. Let's try and capture all renames of existing things in one PR.

[Violeta Hernández]

oh whoops, the first set is actually the extent! glad i caught that

[Wrenna Robson]

Yeah!

[Wrenna Robson]

Somehow you expect it to be the other way round

[Wrenna Robson]

The first set is the objects, the extent of things to which the attributes apply. The second set is the intent, the attributes that are intended by the choice of objects

[Wrenna Robson]

That's how I remember

[Violeta Hernández]

Just updated the PR

[Wrenna Robson]

LGTM :)

[Wrenna Robson]

I think the instances might change a bit. And I'm not sure about those lemmas with "inf" in the name as I think we're now spelling that "min", etc.? But that can be a future piece of work.

[Wrenna Robson]

Do we perhaps want to make a thread in #PR Reviews for this work? It can stay here but people might not see it in maths.

[Violeta Hernández]

I thought we were still using inf and sup for lattices

[Violeta Hernández]

Sure, we can make a PR reviews thread

[Wrenna Robson]

I thought this but I'm not sure. It's certainly not what you get out of simps.

[Violeta Hernández]

We have docs#bot_inf_eq but no docs#bot_min_eq

[Wrenna Robson]

Fair enough then.

[Wrenna Robson]

Incidentally, the completion of the rationals under this gives the extended reals, right? Is there some similar construction that doesn't give you a bounded order if you already have it but otherwise suffices - i.e. gives a conditionally complete order?

Also - I think this follows from the order embedding stuff, but: if you have a linear order on the original type, the completed order is also linear, right?

[Wrenna Robson]

Might be a useful instance

[Violeta Hernández]

Wrenna Robson said:

Incidentally, the completion of the rationals under this gives the extended reals, right? Is there some similar construction that doesn't give you a bounded order if you already have it but otherwise suffices - i.e. gives a conditionally complete order?

Also - I think this follows from the order embedding stuff, but: if you have a linear order on the original type, the completed order is also linear, right?

You can just take out the top and bottom elements. That's what you generally do when you define real numbers as Dedekind cuts, you have to explicitly exclude the cases where either set is empty.

[Wrenna Robson]

Ahhhh

[Violeta Hernández]

And yeah, the completion of a linear order is linear.

[Violeta Hernández]

Not sure what the easiest way to prove this is

[Aaron Liu]

Violeta Hernández said:

Not sure what the easiest way to prove this is

try having an order embedding into LowerSet or UpperSet, and pull back le_total from there, is what I would do

[Violeta Hernández]

Oh of course, the linear order instance on LowerSet is basically exactly what you want

[Violeta Hernández]

instance {α : Type*} [LinearOrder α] : IsTotal (DedekindCut α) (· ≤ ·) where
  total A B := @le_total (LowerSet α) _ ⟨_, A.isLowerSet_fst⟩ ⟨_, B.isLowerSet_fst⟩

noncomputable instance {α : Type*} [LinearOrder α] : LinearOrder (DedekindCut α) := by
  classical exact Lattice.toLinearOrder _

noncomputable instance {α : Type*} [LinearOrder α] : CompleteLinearOrder (DedekindCut α) where
  __ := instCompleteLattice
  __ := instLinearOrder
  __ := LinearOrder.toBiheytingAlgebra

[Wrenna Robson]

Very nice.

[Wrenna Robson]

What does LowerSet correspond to in the concept lingo?

[Wrenna Robson]

(I have actually splurged and bought the Wille book on concept analysis so quite excited for that.)

[Aaron Liu]

Wrenna Robson said:

What does LowerSet correspond to in the concept lingo?

In a preorder α, a complementary pair of a lower set and an upper set corresponds to a Concept α α fun a b => ¬b ≤ a

[Aaron Liu]

Furthermore, this correspondence is an order isomorphism

[Wrenna Robson]

Right, so LowerSet is quite like an extent.

[Wrenna Robson]

Having looked into it, we also have ClosureOperator which is quite closely linked to some of these topics.

[Aaron Liu]

it's a galois connection, sometimes an insertion, sometimes a coinsertion

[Wrenna Robson]

Oh: Chapter 7 of "Introduction to Lattices and Order" actually has the discussion of the Dedekind–MacNeille completion.

[Aaron Liu]

Here's the order iso

import Mathlib

universe u

variable {α : Type u} [Preorder α]

example :
    {s : LowerSet α × UpperSet α // IsCompl (s.1 : Set α) (s.2 : Set α)} ≃o
    Concept α α fun a b => ¬b ≤ a where
  toFun s := {
    extent := s.1.1
    intent := s.1.2
    upperPolar_extent := by
      ext x
      constructor
      · intro hx
        rw [← s.prop.compl_eq, Set.mem_compl_iff]
        intro h
        exact hx h le_rfl
      · intro hx y hy hxy
        apply s.prop.disjoint.notMem_of_mem_left hy
        exact s.1.2.upper hxy hx
    lowerPolar_intent := by
      ext x
      constructor
      · intro hx
        rw [s.prop.eq_compl, Set.mem_compl_iff]
        intro h
        exact hx h le_rfl
      · intro hx y hy hxy
        apply s.prop.disjoint.notMem_of_mem_right hy
        exact s.1.1.lower hxy hx
  }
  invFun s := by
    refine ⟨(⟨s.extent, ?_⟩, ⟨s.intent, ?_⟩), ?_, ?_⟩
    · intro x y hyx hx
      rw [← s.lowerPolar_intent] at hx ⊢
      intro z hz hzy
      exact hx hz (hzy.trans hyx)
    · intro x y hxy hx
      rw [← s.upperPolar_extent] at hx ⊢
      intro z hz hyz
      exact hx hz (hxy.trans hyz)
    · rw [Set.disjoint_iff]
      intro x ⟨hxl, hxr⟩
      simp only [LowerSet.coe_mk, UpperSet.coe_mk] at hxl hxr
      rw [← s.upperPolar_extent] at hxr
      exact hxr hxl le_rfl
    · rw [codisjoint_iff_le_sup]
      intro x _
      simp only [LowerSet.coe_mk, UpperSet.coe_mk, Set.sup_eq_union, Set.mem_union]
      rw [or_iff_not_imp_left]
      intro hx
      rw [← s.lowerPolar_intent] at hx
      simp_rw [lowerPolar, Set.mem_setOf, not_forall, not_not] at hx
      obtain ⟨y, hy, hyx⟩ := hx
      rw [← s.upperPolar_extent] at hy ⊢
      intro z hz hxz
      exact hy hz (hyx.trans hxz)
  left_inv _ := rfl
  right_inv _ := rfl
  map_rel_iff' := by
    intro a b
    simp only [Equiv.coe_fn_mk]
    apply and_self_iff.symm.trans
    conv_lhs =>
      congr
      · rw [← Concept.extent_subset_extent_iff]
      · rw [← Concept.intent_subset_intent_iff]
    simp [← Prod.le_def]

[Wrenna Robson]

Been doing some work on API improvements, started a different branch just to spread out the work a bit.

[Wrenna Robson]

Broadly some analogous types to LowerSet and UpperSet and that.

[Wrenna Robson]

Though I have managed to leave that branch on my home computer

[Wrenna Robson]

Wrenna Robson said:

(I have actually splurged and bought the Wille book on concept analysis so quite excited for that.)

My copy of the Wille book arrived. Gonna try touching concepts again soon.

[Wrenna Robson]

I do find myself wishing we a) had some concept of an order-reversing map, b) had a clear spelling for "Galois connection but it reverses the order".

[Wrenna Robson]

I know that you can use the dual, of course.

[Wrenna Robson]

But I don't like this as an option myself. For one thing - is the natural type of order-reversing maps Aᵒᵈ →o B or A →o Bᵒᵈ?

[Wrenna Robson]

Personally I would like to see a world where we have A →oᵒᵈ B to mean "order-reversing map from A to B", and then an appropriate equivalence between A →oᵒᵈ B and Aᵒᵈ →o B and A →o Bᵒᵈ.

[Wrenna Robson]

But I'm not sure if there's any appetite for this amongst contributors or maintainers.

[Wrenna Robson]

Might make this its own thread.

[Yaël Dillies]

The reason we don't have order-reversing maps, not contravariant functors, is https://xkcd.com/927/

[Bryan Gin-ge Chen]

Wrenna Robson said:

Might make this its own thread.

(linking for future reference: the new thread is at #maths > Order-reversing maps @ 💬)

[Wrenna Robson]

Yaël Dillies said:

The reason we don't have order-reversing maps, not contravariant functors, is https://xkcd.com/927/

The would feel true if we had any standard.

[Antoine Chambert-Loir]

What is the status of your project of constructing the Dedekind-MacNeille completion?

[Wrenna Robson]

God I can't even remember where we got to. I think I got lost down an order whole. I really need a better way of tracking my Mathlib and Lean projects.

[Violeta Hernández]

I completely forgot about this. Once I was able to use concepts to define surreal gaps i didn't really continue working on this.

[Violeta Hernández]

There should be an open PR of mine defining an alias for the DM completion, I'll see if I can resurrect it.

[Violeta Hernández]

Ah yes, #26966

[Violeta Hernández]

Note that if you want to work with the DM completion right now, you already can:

abbrev DedekindCut [Preorder α] := Concept α α (· ≤ ·)

[Violeta Hernández]

I think what stopped me was @Wrenna Robson figuring out that some of my definitions could be generalized

[Violeta Hernández]

Ah! I'm glad I left a comment about this:

As a sidenote, the PR actually got drafted because it turns out this is not the most general definition! In any concept lattice, you can define two maps ofObject and ofAttribute; these just happen to give the same map in this special case.

[Violeta Hernández]

I'm not currently in the middle of any other major projects, so I think I can get this one over the finish line

[Wrenna Robson]

Happy to review it btw

[Violeta Hernández]

I notice your branch defines ofObjects and ofAttributes, for a set rather than a single element

[Violeta Hernández]

Do you think it's worth having both the set/element versions, or should we stick to one (or the other?)

[Wrenna Robson]

I think there was a reason I did that certainly! But I can't remember what it was.

[Violeta Hernández]

I probably need to read the document you sent me in full

[Wrenna Robson]

I'm sorry ;_;. I really got quite keen for this but then life happened.

[Violeta Hernández]

Ah, don't worry

[Wrenna Robson]

And I just kept finding stuff that I wanted to change

[Violeta Hernández]

I also am juggling like five Lean projects at any given point

[Wrenna Robson]

Mood

[Wrenna Robson]

I just tend to get bogged down in reviews or whatever

[Wrenna Robson]

And then never have time to get stuff finished

[Violeta Hernández]

yeah, I get you

[Violeta Hernández]

A lot of my work is kind of niche and so it often gets trapped in review hell

[Violeta Hernández]

Just opened #29995 and #29996. The former just adds a few lemmas I needed in the CGT repo, and the latter is just some small stylistic changes to the file.

[Violeta Hernández]

Ah nvm, I see that the work on your branch actually allows much simpler definitions for the instances! I think I'll replace #29996 with that.

[Wrenna Robson]

I'm glad that past me was smart and cool or whatever

[Violeta Hernández]

Specifically, I think I'll replace #29996 with a PR that defines IsIntent / IsExtent and uses them to golf the definitions of the lattice structure on concepts

[Violeta Hernández]

(You don't mind me opening the PR and adding you as a coauthor, do you?)

[Wrenna Robson]

I do not.

[Wrenna Robson]

I think you'll do good work here and I'm enthusiastic about contributing if I can, I just know I can't commit to it right now

[Violeta Hernández]

The new and improved #29996 is ready!

[Violeta Hernández]

Your usage of simps! was really clever, I was able to get rid of a huge block of lemmas which are now autogenerated

[Wrenna Robson]

Oh nice

[Wrenna Robson]

Should I look at #29995 first?

[Violeta Hernández]

It's quite smaller, so it might be easier to start there yeah

[Violeta Hernández]

Even smaller now that I realize I can use simps! there too

[Wrenna Robson]

Just made a commend to that extent! One sec while I finish

[Wrenna Robson]

Some comments added

[Wrenna Robson]

In general I would say that we do NOT here use the same approach that LowerSet and UpperSet use (where they have structure types that essentially correspond to upper and lower sets, which then use the predicate). I think that is fine - I just want to note the difference of approach.

[Wrenna Robson]

BUT having said this

[Wrenna Robson]

if you define an Extent and Intent type, the point is that they are order-isomorphic with the Concept lattice.

[Wrenna Robson]

i.e. I think it is true that a Concept is uniquely determined by its extent and its intent.

[Wrenna Robson]

Do we have a definition of the upper and lower closure? i.e. analogous to upperClosure and lowerClosure?

[Wrenna Robson]

I remember that I was playing around with this, and I am not sure I had found my favoured description.

[Wrenna Robson]

But all these concepts stuff is quite closely tied into closure operators and the like.

[Violeta Hernández]

I don't really think we should define an Extent/Intent type. In an ideal world, I don't believe we would have defined separate UpperSet/LowerSet types either.

[Violeta Hernández]

Wrenna Robson said:

Do we have a definition of the upper and lower closure? i.e. analogous to upperClosure and lowerClosure?

Isn't that just upperBounds and lowerBounds?

[Wrenna Robson]

So in this context I mean like "the smallest extent that contains a set" or whatever

[Wrenna Robson]

I guess these was the ofObjects or ofAttributes thing, right?

[Wrenna Robson]

Like if I have a set s, lowerPolar r (upperPolar r s) is the extent closure of it.

[Wrenna Robson]

That set is an extent.

[Wrenna Robson]

So a set whose extent closure is equal to itself is an extent

[Wrenna Robson]

same (dual) for intents

[Violeta Hernández]

Hm you're right, the upper closure would be upperBounds (lowerBounds s)

[Violeta Hernández]

No, I don't believe we have a definition for that

[Wrenna Robson]

https://en.wikipedia.org/wiki/Closure_operator

[Violeta Hernández]

Oh wait I'm sorry I completely misunderstood your question

[Violeta Hernández]

You're asking whether we should have upperClosure r s = upperPolar r (lowerPolar r s) as a definition?

[Wrenna Robson]

Yep!

[Wrenna Robson]

btw I agree about the separate types I think.

[Wrenna Robson]

Well you would call it the extentClosure probably.

[Wrenna Robson]

Obviously we had extentClosure previously, but the definition was not correct as we know

[Wrenna Robson]

Like if you look at the "formal contexts and concepts" heading here: https://en.wikipedia.org/wiki/Formal_concept_analysis

[Violeta Hernández]

hmm... it's a tough call. I feel like it might be too simple of an object to have, considering it's just the composition of two other functions with extensive API

[Wrenna Robson]

basically taking two primes is a closure

[Wrenna Robson]

Violeta Hernández said:

hmm... it's a tough call. I feel like it might be too simple of an object to have, considering it's just the composition of two other functions with extensive API

I somewhat suspect this. It should probably be an abbrev if it is defined.

[Violeta Hernández]

What about instead having extentClosure be a docs#ClosureOperator on Set α?

[Wrenna Robson]

I think that would make sense (and it... is that, I think?)

[Wrenna Robson]

(Yes.)

[Wrenna Robson]

We have the GaloisConnection between upperPolar and lowerPolar, right?

[Violeta Hernández]

that way it's not just the composition of these two functions

[Violeta Hernández]

We do, yes

[Wrenna Robson]

(Possibly you need to stickl some duals in there IDK).

[Wrenna Robson]

Because I think the closure operator will have a way of being made from the Galois Connection

[Wrenna Robson]

GaloisConnection.closureOperator

[Violeta Hernández]

It's probably easy enough to construct it directly with the API we already have

[Violeta Hernández]

Ah, nice

[Wrenna Robson]

If we're lucky that will even be nicely defeq when applied to the obvious thing.

[Wrenna Robson]

It's a really neat construction really - you go from this set with an arbitrary relation. and use that relation to construct this particular sublattice of the power set (the extents/the intents).

[Wrenna Robson]

which is complete!

[Wrenna Robson]

And then in particular if your original relation was <=... then when your original type embeds into this lattice, that is the completion and everything is respected.

[Violeta Hernández]

Wrenna Robson said:

Violeta Hernández said:

hmm... it's a tough call. I feel like it might be too simple of an object to have, considering it's just the composition of two other functions with extensive API

I somewhat suspect this. It should probably be an abbrev if it is defined.

I've learned the hard way that abbrev isn't nearly as nice as you'd want it to be

[Wrenna Robson]

It certainly isn't a catch-all solution.

[Violeta Hernández]

I just opened #30001 defining ofObjects and ofAttributes. This depends on #29996 for some lemmas, though.

[Violeta Hernández]

I think with that, everything on your branch has a PR now :slight_smile:

[Wrenna Robson]

I would change ofObjects_extent to ofObjects_apply_extent maybe (which lets you use simps?)

[Wrenna Robson]

Really though it feels like maybe simps should generate it as a prefix (extent_ofObjects)

[Violeta Hernández]

It's the eternal debate of dot notation

[Wrenna Robson]

Indeed

[Wrenna Robson]

Did you define that closure operator?

[Violeta Hernández]

I think the majority opinion is that foo.bar should be written down as bar_foo, but unfortunately simps disagrees with us

[Violeta Hernández]

I added the closure operator to #30001, though I don't really use it at all

[Wrenna Robson]

I note that (ofObjects r s).extent is a shorter spelling of it.

[Wrenna Robson]

I did have some comments on the other ones I can see you've not done? In particular I think it would be good to explictly have both sup and inf when defining the Lattice.

[Wrenna Robson]

i.e. as well as sup := (· ⊔ ·), also explictly give inf.

[Violeta Hernández]

Wrenna Robson said:

I did have some comments on the other ones I can see you've not done? In particular I think it would be good to explictly have both sup and inf when defining the Lattice.

I did respond to it, I mentioned that the SemilatticeInf instance already takes care of inf

[Wrenna Robson]

No I know.

[Wrenna Robson]

I'm saying you shouldn't leave it to that, it's often good in such cases to expressly define it.

[Wrenna Robson]

So that it is definitely defeq to the thing you want.

[Violeta Hernández]

you mean, add a field inf := (· ⊓ ·)?

[Wrenna Robson]

Ohh except - right

[Wrenna Robson]

Yes

[Violeta Hernández]

that feels a bit silly, since the inf instance that's inferred is in fact def-eq to the inf instance that's inferred

[Wrenna Robson]

Doesn't hurt to make it explict

[Wrenna Robson]

Arguably instSemilatticeInfConcept adds very little.

[Violeta Hernández]

It gets all three inf fields from the Lattice instance done at once

[Violeta Hernández]

As well as giving the PartialOrder instance

[Wrenna Robson]

Yes but you could just directly define the lattice. It isn't like it only exists under a certain constraint

[Violeta Hernández]

the Lattice instance uses some auxiliary theorems that we need the PartialOrder instance to even state

[Wrenna Robson]

also not quite sure about theorem ext' - again I just don't like primes! But extExtent and extIntent wouldn't be very ergonomic. It's just that I am not sure about breaking the symmetry

[Wrenna Robson]

Violeta Hernández said:

the Lattice instance uses some auxiliary theorems that we need the PartialOrder instance to even state

Ahhh fair

[Violeta Hernández]

Wrenna Robson said:

also not quite sure about theorem ext' - again I just don't like primes! But extExtent and extIntent wouldn't be very ergonomic. It's just that I am not sure about breaking the symmetry

Agree, that's why I instead added the docstrings

[Wrenna Robson]

I would probably use PartialOrder.lift to create the partial order

[Violeta Hernández]

Wrenna Robson said:

Doesn't hurt to make it explict

Making the inf field explicit makes it so that the other fields inf_le_left, inf_le_right, le_inf can no longer be inferred

[Wrenna Robson]

Alas.

[Violeta Hernández]

Wrenna Robson said:

I would probably use PartialOrder.lift to create the partial order

Well, but then we'd have to prove those three theorems instead of just getting them for free

[Wrenna Robson]

No, true...

[Wrenna Robson]

Btw do we have the theorem that c <= d (c d concepts) iff c.extent <= d.extent and iff d.intent <= c.intent?

[Violeta Hernández]

of course

[Wrenna Robson]

I can't see them

[Wrenna Robson]

but I thought we must do

[Wrenna Robson]

what are they called?

[Violeta Hernández]

docs#Concept.extent_subset_extent_iff

[Wrenna Robson]

That... doesn't seem to exist?

[Wrenna Robson]

In either file?

[Violeta Hernández]

edited

[Wrenna Robson]

aha!

[Wrenna Robson]

yes I always forget that we tend to use subset here

[Wrenna Robson]

How are Concept α β r and Concept α β (fun a b => ¬r a b) related btw? Are they at all?

[Wrenna Robson]

Oh also, where actually is the definition of the Dedekind-MacNeille completion in all this?

[Violeta Hernández]

Wrenna Robson said:

How are Concept α β r and Concept α β (fun a b => ¬r a b) related btw? Are they at all?

If s is an extent in the former, then I think sᶜ should be an extent in the latter? likewise with the intent.

[Wrenna Robson]

That feels right.

[Violeta Hernández]

Wrenna Robson said:

Oh also, where actually is the definition of the Dedekind-MacNeille completion in all this?

That's a completely different PR, which I want to remake using #30001

[Wrenna Robson]

Got it.

[Wrenna Robson]

Violeta Hernández said:

Wrenna Robson said:

How are Concept α β r and Concept α β (fun a b => ¬r a b) related btw? Are they at all?

If s is an extent in the former, then I think sᶜ should be an extent in the latter? likewise with the intent.

It basically just occured to me that the link between the Concept for < and the concept for <= might be a combination of this plus the swap one.

[Violeta Hernández]

In the linear order case, maybe

[Wrenna Robson]

Yes.

[Violeta Hernández]

I might be wrong about this, but I think that in any partial order, the <-concept lattice looks like the Dedekind completion, except that every element in the original order is associated to two elements that cover each other, instead of just one

[Wrenna Robson]

Hmm interesting.

[Violeta Hernández]

At least that happens in the linear order case

[Violeta Hernández]

I don't see a reason why it shouldn't happen in the partial order case too

[Violeta Hernández]

To be more specific, to embed an element of a poset into its Dedekind completion, you use the map fun x ↦ (Iic x, Ici x)

[Violeta Hernández]

but in the <-concept lattice, you can use either of fun x ↦ (Iio x, Ici x) or fun x ↦ (Iic x, Ioi x)

[Wrenna Robson]

Yeah that makes sense.

[Wrenna Robson]

Man that feels the wrong way round

[Wrenna Robson]

like it feels like it should be (Ici x, Iic x)

[Wrenna Robson]

But then you'd have to reverse intent and extent I guess

[Aaron Liu]

Violeta Hernández said:

I might be wrong about this, but I think that in any partial order, the <-concept lattice looks like the Dedekind completion, except that every element in the original order is associated to two elements that cover each other, instead of just one

Remember linear orders are automatically a lot of things

[Aaron Liu]

I have a four element poset whose <-concept lattice is a three element chain

[Aaron Liu]

and it's not always true for linear orders either since if it has a top or bot

[Yijun Yuan]

In my work on Hader-Narasimhan theory, I implemented the Dedekind-MacNeille completion DM(X) of any partially ordered set X (the minimal complete lattice containing a given partially ordered set), and showed that

1. If the order on X is linear, then the order on DM(X) is also linear.
2. The universal property of DM(X): any order embedding X→Y, with Y a complete lattice, factors through the canonical embedding X→DM(X).

What I do not formalize: The denseness of X in DM(X) (meet-dense, join-dense...)

I don't know if this is helpful

Code: https://github.com/YijunYuan/HarderNarasimhan/blob/master/HarderNarasimhan/OrderTheory/DedekindMacNeilleCompletion.lean

When working on this project, I'm not aware of this thread :rolling_on_the_floor_laughing:

[Violeta Hernández]

(deleted)

[Violeta Hernández]

Aaron Liu said:

I have a four element poset whose <-concept lattice is a three element chain

How come?

[Aaron Liu]

it just is

[Aaron Liu]

I calculated it

[Aaron Liu]

Everything is finite so

[Violeta Hernández]

Ok, let me rephrase, what's your example?

[Aaron Liu]

uhm

[Aaron Liu]

how do I describe this

[Aaron Liu]

it's the specialization order on the pseudocircle

[Violeta Hernández]

Hey, wait, stop, wait a second

[Violeta Hernández]

Isn't the Dedekind-MacNeille completion of α literally just LowerSet α?

[Wrenna Robson]

That seems like it would be isomorphic. But morally all that stuff is kinda a special case of the concept stuff.

[Aaron Liu]

no

[Aaron Liu]

it's not

[Violeta Hernández]

ok thank goodness

[Wrenna Robson]

Oh yeah the implication is the other way round.

[Aaron Liu]

counting argument the dedekind completion of singleton is singleton but lower sets is two-chain

[Wrenna Robson]

What is two-chain?

[Aaron Liu]

linear order with two elements

[Wrenna Robson]

Right.

[Wrenna Robson]

Yeah I think LowerSet is not minimal in that sense. You can presumably embed into it?

[Aaron Liu]

if the order is linear

[Wrenna Robson]

Right

[Aaron Liu]

Wrenna Robson said:

That seems like it would be isomorphic. But morally all that stuff is kinda a special case of the concept stuff.

It is a special case not just morally but literally

[Wrenna Robson]

Well it isn't in terms of how it is defined.

[Aaron Liu]

Aaron Liu said:

Here's the order iso

import Mathlib

universe u

variable {α : Type u} [Preorder α]

example :
    {s : LowerSet α × UpperSet α // IsCompl (s.1 : Set α) (s.2 : Set α)} ≃o
    Concept α α fun a b => ¬b ≤ a where
  toFun s := {
    extent := s.1.1
    intent := s.1.2
    upperPolar_extent := by
      ext x
      constructor
      · intro hx
        rw [← s.prop.compl_eq, Set.mem_compl_iff]
        intro h
        exact hx h le_rfl
      · intro hx y hy hxy
        apply s.prop.disjoint.notMem_of_mem_left hy
        exact s.1.2.upper hxy hx
    lowerPolar_intent := by
      ext x
      constructor
      · intro hx
        rw [s.prop.eq_compl, Set.mem_compl_iff]
        intro h
        exact hx h le_rfl
      · intro hx y hy hxy
        apply s.prop.disjoint.notMem_of_mem_right hy
        exact s.1.1.lower hxy hx
  }
  invFun s := by
    refine ⟨(⟨s.extent, ?_⟩, ⟨s.intent, ?_⟩), ?_, ?_⟩
    · intro x y hyx hx
      rw [← s.lowerPolar_intent] at hx ⊢
      intro z hz hzy
      exact hx hz (hzy.trans hyx)
    · intro x y hxy hx
      rw [← s.upperPolar_extent] at hx ⊢
      intro z hz hyz
      exact hx hz (hxy.trans hyz)
    · rw [Set.disjoint_iff]
      intro x ⟨hxl, hxr⟩
      simp only [LowerSet.coe_mk, UpperSet.coe_mk] at hxl hxr
      rw [← s.upperPolar_extent] at hxr
      exact hxr hxl le_rfl
    · rw [codisjoint_iff_le_sup]
      intro x _
      simp only [LowerSet.coe_mk, UpperSet.coe_mk, Set.sup_eq_union, Set.mem_union]
      rw [or_iff_not_imp_left]
      intro hx
      rw [← s.lowerPolar_intent] at hx
      simp_rw [lowerPolar, Set.mem_setOf, not_forall, not_not] at hx
      obtain ⟨y, hy, hyx⟩ := hx
      rw [← s.upperPolar_extent] at hy ⊢
      intro z hz hxz
      exact hy hz (hyx.trans hxz)
  left_inv _ := rfl
  right_inv _ := rfl
  map_rel_iff' := by
    intro a b
    simp only [Equiv.coe_fn_mk]
    apply and_self_iff.symm.trans
    conv_lhs =>
      congr
      · rw [← Concept.extent_subset_extent_iff]
      · rw [← Concept.intent_subset_intent_iff]
    simp [← Prod.le_def]

[Wrenna Robson]

But yes.

[Yijun Yuan]

Sorry to interrupt, but what's the theme of the current discussion?

[Violeta Hernández]

@Yijun Yuan Just checked your branch. I think everything in there is covered by my PR (with much simpler proofs)

[Yijun Yuan]

Violeta Hernández said:

Yijun Yuan Just checked your branch. I think everything in there is covered by my PR (with much simpler proofs)

Great!

[Yijun Yuan]

Then maybe another remark is needed in my preprint :rolling_on_the_floor_laughing:

[Violeta Hernández]

Just updated #26966. This now contains a CompleteLinearOrder (DedekindCut α) instance.

[Violeta Hernández]

@Aaron Liu Ah, that explains it. So the modified Dedekind cut construction of surreals is really the ⧏-concept lattice, which happens to match the <-concept lattice in the linear order case.

[Wrenna Robson]

Have you got that DedekindCut.of is surjective on a Complete Lattice?

[Aaron Liu]

Violeta Hernández said:

Aaron Liu Ah, that explains it. So the modified Dedekind cut construction of surreals is really the ⧏-concept lattice, which happens to match the <-concept lattice in the linear order case.

that's what I said

[Wrenna Robson]

Or related things - like, if the underlying type is a CompleteSemilatticeSup, then the sSup operations are compatible (or whatever is true).

[Aaron Liu]

The <-concept lattice doesn't seem to be anything I know in the case of a non-linear order

[Wrenna Robson]

I guess of( sSup {s})

Wrenna Robson said:

Or related things - like, if the underlying type is a CompleteSemilatticeSup, then the sSup operations are compatible (or whatever is true).

Maybe this simply follows from it being an order embedding, IDK.

[Violeta Hernández]

Wrenna Robson said:

Have you got that DedekindCut.of is surjective on a Complete Lattice?

I can add that, it follows directly from the factor theorem

[Aaron Liu]

Surjective order embedding is order iso?

[Wrenna Robson]

Basically "if sup, inf, bot, top, sSup, sInf have sensible definitions, those definitions are compatible with the completion", that kind of thing.

[Wrenna Robson]

For me that is kind of the key final property - "if these things mean

Aaron Liu said:

Surjective order embedding is order iso?

Yeah I am not sure I can see "when it's a Complete Lattice already this is an order iso", though it surely follows!

[Aaron Liu]

I think of this as "adjoining" a sSup and sInf for every set in a way that makes it a complete lattice so if a set already has a sup or inf then it's "forced" to be the same as the existing one

[Wrenna Robson]

Aye

[Aaron Liu]

Probably translates to a statement involving docs#IsGLB and a statement involving docs#IsLUB

[Wrenna Robson]

You could define a map universal_sSup for instance (bad name) which is basically "take the sSup of a set into the Dedekind completion".

[Wrenna Robson]

And one could imagine some map on the Dedekind completion which is essentially the "go back to the original type if you can (because it is in the range of DedekindCut.of)".

[Aaron Liu]

I think this is something like "the map into the completion is bicontinuous"

[Wrenna Robson]

Which reminds me: I think DedekindCut.of should be protected.

[Violeta Hernández]

docs#FreeGroup.of and co. aren't protected so I think we should be fine

[Wrenna Robson]

Ah OK

[Violeta Hernández]

Just added of as an order isomorphism to the PR

[Wrenna Robson]

Nice.

[Violeta Hernández]

There's probably more stuff to be done, but I'd rather not be trapped in scope creep.

[Wrenna Robson]

Aye

[Violeta Hernández]

Question: does ofIso count as a proof of the fundamental theorem of concept lattices?

[Aaron Liu]

what's the fundamental theorem

[Wrenna Robson]

I feel like you would need a proof that if something is isomorphic to its Dedekind Cut, it is a complete lattice, but given the dedekind cut is a complete lattice that is surely a one-line proof.

[Violeta Hernández]

As I understand it, the fundamental theorem of concept lattices is "every concept lattice is a complete lattice, and every complete lattice is isomorphic to a concept lattice"

[Violeta Hernández]

we have in fact now proved both

[Wrenna Robson]

Depends on the statement I think but I would say it's basically there

[Violeta Hernández]

image.png
This seems to be what I'm saying

[Wrenna Robson]

Aye

[Wrenna Robson]

There is some stuff about infimum-dense and supremum-dense stuff that are in some statements of it I think

[Violeta Hernández]

Theorem 3.9 does seem to be a bit more detailed
image.png

[Wrenna Robson]

Yes I think you have the "in particular".

[Wrenna Robson]

I don't think mathlib contains concept of join-dense and meet-dense so that feels like a future PR

[Violeta Hernández]

Reading the statement from 3.10 I don't really get the impression that the entirety of 3.9 is part of the fundamental theorem

[Violeta Hernández]

It seems that the fundamental theorem is the characterization of concept lattices, rather

[Violeta Hernández]

Basically what I'm asking is whether I can get rid of the todo on the module docstring

[Wrenna Robson]

Right! I feel like morally yes but expect to justify that to reviewers so do make a note.

[Violeta Hernández]

@Aaron Liu Wait, isn't LowerSet Surreal the same as Cut?

[Violeta Hernández]

I think that's what your order iso proves

[Aaron Liu]

Violeta Hernández said:

Aaron Liu Wait, isn't LowerSet Surreal the same as Cut?

Yes???

[Aaron Liu]

What's the confusion here

[Violeta Hernández]

that I got into concepts for nothing

[Aaron Liu]

no it's for the defeqs

[Violeta Hernández]

oh yeah this is in the concept lattice PDF
image.png

[Aaron Liu]

neat