Completion of a linear order

Stream: Is there code for X?

[Eric Paul]

Is there a good way to talk about the completion or the conditional completion of a linear order?

[Kenny Lau]

@Violeta Hernández

[Violeta Hernández]

I have an open PR for the Dedekind completion of a poset. What is the conditional completion?

[Aaron Liu]

completion without the top or bottom maybe

[Eric Paul]

Oh great, I'm glad to hear there's a relevant PR for it! Let me know if I can do anything helpful for that. I want to be able to talk about this for linear orders, in particular the extension of an automorphism on a linear order to one on its completion.

For the conditionally complete, as Aaron said, it's the same thing as the completion but without the top and bottom points (docs#ConditionallyCompleteLinearOrder).

[Violeta Hernández]

I suspect it might be easier to make a more general construction for "order without bottom and top"

[Kenny Lau]

if you remove the bottom and top, what about the new bottom and top

[Eric Paul]

That makes sense, especially because sometimes I'd like to keep one of the endpoints

[Violeta Hernández]

Kenny Lau said:

if you remove the bottom and top, what about the new bottom and top

Well, to be more specific, my proposal is to make something like WithoutTop α = {x : α // x ≠ ⊤}

[Violeta Hernández]

though of course there's the question of whether this is any better than just working with the subtype directly

[Kenny Lau]

I think you can relax the hypothesis

[Violeta Hernández]

Sure, {x : α // ¬ IsTop x}, or {x : α // ¬ IsMax x} or whatever

[Kenny Lau]

structure NoTop {α} [LT α] where
  val : α
  exists_gt : ∃ x, val < x

[Kenny Lau]

yeah, exactly

[Aaron Liu]

Eric Paul said:

For the conditionally complete, as Aaron said, it's the same thing as the completion but without the top and bottom points (docs#ConditionallyCompleteLinearOrder).

What if your original order already has a top or bottom, then the completion won't add a new top or bottom so are you getting rid of the original one?

[Eric Paul]

I only care about it in the case where the original order does not have a top and bottom. In other words, if there was a top and bottom in the original order, I don’t remove those.

[Kenny Lau]

i feel like all o' yall are overcomplicating it, are we just saying that the lowerset has to be nonempty and not the top set?

[Aaron Liu]

Kenny Lau said:

i feel like all o' yall are overcomplicating it, are we just saying that the lowerset has to be nonempty and not the top set?

what does that mean

[Aaron Liu]

can you explain

[Eric Paul]

You can create the conditional completion by only taking cuts where both the lower and upper part of the cut are nonempty. I think that's what Kenny is saying.

[Aaron Liu]

oh yeah

[Aaron Liu]

I think that's true

[Kenny Lau]

btw does this resolve the issue of duplicating Q?

[Eric Paul]

What is the issue of duplicating Q?

[Kenny Lau]

if you try to complete Q "naively", you end up with R but with every point of Q duplicated

[Eric Paul]

My understanding of the completion of a linear order is that you have cuts (I, J). A cut (I, J) is a gap if I has no top point and J has no bottom point. To complete a linear order, you add a point for every gap. With this definition, the completion of Q is R (where I exclude cuts where the upper or lower part are empty).

[Violeta Hernández]

the way my PR does things is slightly different, a cut is a pair (I, J) where J is the set of upper bounds of I and viceversa

[Violeta Hernández]

so for each rational q, the cut looks like (Iic q, Ici q)

[Violeta Hernández]

(this is just the concept lattice of the ≤ relation on rationals)

[Violeta Hernández]

(the "naive" completion is the concept lattice of <, or rather the not ≥ relation)

[Eric Paul]

For ≤, isn't q an upper bound and lower of bound q? Why isn't the cut for q (Iic q, Ici q)?

[Violeta Hernández]

because I wrote it wrong haha

[Aaron Liu]

this solves the issue of duplicating Q but also generalizes to orders which are not linear

[Aaron Liu]

it's pretty nice

[Eric Paul]

Cool, that makes sense

[Violeta Hernández]

I realize I never linked to my PR: #26966

[Violeta Hernández]

There's still a long chain of dependents for it, though