Formalizing Dedekind cuts

Stream: new members

[Dan Stanescu]

Since this was deemed worth pursuing, I may take a cut at it. To start with, I'm wondering if there's anyone else who's been planning that already. I also want to check if my choices for the structure fields and their names seem readable enough. BTW, what is happening with the mathlib nursery, there doesn't seem to be any contribution for the last two years?

structure dedekind_cut :=
(carrier     : set ℚ)
(not_empty   : carrier.nonempty)
(not_all     : ∃ r : ℚ, r ∉ carrier)
(closed_down : ∀ s ∈ carrier, ∀ r : ℚ, r ≤ s → r ∈ carrier )
(no_greatest : ∀ r ∈ carrier, ∃ s ∈ carrier,  r < s )

[Mario Carneiro]

You could generalize Q in this definition

[Bryan Gin-ge Chen]

The nursery is effectively moribund. Probably we should formally "archive" it on GitHub.

[Mario Carneiro]

In particular, I think you will find that it is easier to define the positive reals as dedekind cuts of positive rationals than using all rationals (especially when it comes to multiplication)

[Mario Carneiro]

also, you will want to be able to talk about dedekind cuts of real numbers when showing completeness

[Kevin Buzzard]

One technical problem with Dedekind cuts is what to with the rationals -- should the rational be in the top cut or the bottom one? Someone recently explained to me that one solution to this is to say "neither", and formalise Dedekind cuts with the axiom that if a<b then either a is in the bottom cut or b is in the top cut. This forces the union of the two cuts to be either all the rationals, or all but one.

[Mario Carneiro]

In Dan's definition you don't bother with the top cut, and the bottom cut is open

[Mario Carneiro]

I think this is the Right Way to do it

[Alex J. Best]

I think defining cuts in general would be good. I did some related stuff in https://github.com/leanprover-community/mathlib/pull/3292 but without really defining cuts as a structure, just giving a cut as a set and proving those properties separately. Might be cool to go as general as https://en.wikipedia.org/wiki/Dedekind%E2%80%93MacNeille_completion though

[Kevin Buzzard]

Aah I see -- yes, this is a nice slick way to do it. You'll still have to be careful when multiplying -sqrt(2) by itself.

[Mario Carneiro]

If you define positive reals then there is no -sqrt(2)

[Mario Carneiro]

Given positive reals, you can just define reals the same way you get int from nat

[Kevin Buzzard]

I agree that this looks like the most painless approach. I've had students doing Dedekind reals in the past and it's surprising how annoying it is compared to the Cauchy sequences approach.

[Dan Stanescu]

I was just looking at the Wikipedia definition and the one in P.J. Cameron's book "Sets, Logic and Categories".

[Mario Carneiro]

If you are aiming for mathlib, expect it to be generalized to unrecognizability :slight_smile:

[Dan Stanescu]

Although the latter favors using both the lower and the upper cut, Wiki goes for the lower only. Which I think it is an advantage.

[Mario Carneiro]

You can do the D-MN completion with only lower cuts

[Mario Carneiro]

in fact the wiki definition does it that way

[Dan Stanescu]

Dedekind cuts have their advantage (unique vs. equivalence class) so it's good to have them.

Thank you all for the input and I'm glad I asked. Will take a look at the generalization pointed to by @Alex J. Best . My dream goal is to have an undergraduate student working on this, so hopefully it can be PR'd into mathlib incrementally.

[Jireh Loreaux]

Hi, my name is Jireh Loreaux, and since this is the new members stream I thought I would introduce myself. I am a mathematician at Southern Illinois University Edwardsville. I've been tracking the Lean project and mathlib for about two years, but have finally had a few weeks to spend devoted to learning. After working my way through the various tutorials and LftCM2020 materials, I decided to try and implement something nontrivial on my own to see what kinds of problems I would run into once I was unguided.

So, I decided to implement the real numbers as Dedekind cuts of rationals because I noticed it wasn't in mathlib (I didn't think to check for PRs, and I hadn't gotten comfortable with Zulip yet). I am most of the way through it, and I think I have learned as much from this particular project as I can. I could continue it and create a PR, but I'm not clear from the above thread if this is something someone else is already in the process of implementing.

Alternatively, I work in C*-algebras and operator theory, and I see that the mathlib theory really only goes up to Banach spaces and linear maps between them. So, I could start working on a PR in this direction as well, but I'm not sure how best to determine the WIPs of everyone else on this topic.

[Heather Macbeth]

Hi, welcome! We'll be very happy to have your contributions.

[Heather Macbeth]

Some ongoing things that might be interesting to you: @Scott Morrison has proved the Bell and Tsirelson inequalities, although in a slightly more general context than the classical C*-algebra context -- there are open PRs for these:
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Bell.20and.20Tsirelson.20inequalities
And @Frédéric Dupuis has been setting up Hilbert space theory, currently he has an open PR for the Riesz representation theorem:
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Hilbert.20space.20is.20isometric.20to.20its.20dual

[Heather Macbeth]

Anything in the Hilbert space, C*-algebra, etc direction would be enthusiastically welcomed. Frederic and Scott probably have ideas for the natural next steps.

I think there would be some debate about whether the Dedekind-cut construction of the reals is appropriate for mathlib, given that there is another construction currently implemented. On the other hand, there is an open PR for the characterization of the reals as the unique conditionally complete linear ordered field, #3292, I think the author @Alex J. Best has other priorities now, so if that's of interest to you, you could take it over.

[Frédéric Dupuis]

Welcome! I would definitely encourage you to work on C*-algebras and operator theory, we are barely getting started in that direction as Heather said.

[Jireh Loreaux]

Great! Thanks for the pointers to the relevant chats and PRs. I'll have a look and see where I can make myself useful sometime within the next week.