Zulip Chat Archive

Stream: maths

Topic: reals are unique complete ordered field


view this post on Zulip Kevin Buzzard (Aug 09 2018 at 08:50):

The reals are the unique complete ordered field up to unique isomorphism. Is this in Lean already? I thought it might be a good exercise for a student. @Patrick Massot does "complete" here mean "an ordered field inherits a topology from the order, and the associated uniform space is complete"? Last week I didn't know what that even meant. Is that the same as asking that any non-empty bounded set has a least upper bound?

I think Reid Barton once commented that because of this theorem, one should not prove theorems about the reals, one should instead prove theorems about complete ordered fields :-)

view this post on Zulip Mario Carneiro (Aug 09 2018 at 08:56):

I think there is a more useful way to characterize this property: real.cast

view this post on Zulip Mario Carneiro (Aug 09 2018 at 08:57):

Any complete field has a unique continuous field hom from the reals

view this post on Zulip Mario Carneiro (Aug 09 2018 at 08:59):

Also, I think we have a good bit of the infrastructure already, since it was originally used to define functions like addition on the reals by continuous extension from rat.add

view this post on Zulip Andrew Ashworth (Aug 09 2018 at 09:00):

iirc Reid mentioned that because a synthetic, axiom based real number allowed his code to run much faster

view this post on Zulip Mario Carneiro (Aug 09 2018 at 09:00):

That's often true

view this post on Zulip Mario Carneiro (Aug 09 2018 at 09:01):

concrete constructions have the drawback that lean can start unfolding them

view this post on Zulip Mario Carneiro (Aug 09 2018 at 09:11):

Here, I'll get you started:

def real.cast {α} [topological_space α] [division_ring α] : ℝ → α :=
dense_embedding_of_rat.extend coe

Can you prove that this has all the same properties as rat.cast? What is the analogue of rat.eq_cast?

view this post on Zulip Johan Commelin (Aug 09 2018 at 09:16):

Mario, did you just write down a map from real to rat?

view this post on Zulip Mario Carneiro (Aug 09 2018 at 09:17):

heh, I guess I did

view this post on Zulip Johan Commelin (Aug 09 2018 at 09:17):

Ughh. The mathematician in me is worried, and crying, and has a huge headache. This is not a nice map, is it?

view this post on Zulip Mario Carneiro (Aug 09 2018 at 09:18):

It is under more assumptions

view this post on Zulip Mario Carneiro (Aug 09 2018 at 09:18):

extend_eq requires that the space be t2

view this post on Zulip Mario Carneiro (Aug 09 2018 at 09:18):

and tendsto_extend needs that it is regular

view this post on Zulip Mario Carneiro (Aug 09 2018 at 09:18):

I guess Q is not a regular space?

view this post on Zulip Johan Commelin (Aug 09 2018 at 09:18):

But, to which rat does that map send pi or e?

view this post on Zulip Johan Commelin (Aug 09 2018 at 09:19):

I guess we'll never know... because of computability

view this post on Zulip Mario Carneiro (Aug 09 2018 at 09:19):

If the limit is not defined, it maps to an arbitrary constant in Q

view this post on Zulip Johan Commelin (Aug 09 2018 at 09:20):

Right, so it is the identity on rationals and maps the rest to 57 (or 37, if you ask Kevin).

view this post on Zulip Mario Carneiro (Aug 09 2018 at 09:21):

Actually it is classical.choice (_ : nonempty Q)

view this post on Zulip Patrick Massot (Aug 09 2018 at 09:22):

Kevin: https://en.wikipedia.org/wiki/Real_number#%22The_complete_ordered_field%22

view this post on Zulip Mario Carneiro (Aug 09 2018 at 09:23):

Oh, I was wrong, you need more than just regular space for it to be defined, you need this condition

(hf : ∀b, ∃c, tendsto f (vmap e (nhds b)) (nhds c))

view this post on Zulip Mario Carneiro (Aug 09 2018 at 09:24):

There should be a simple assumption giving this property, but I guess you need a uniform structure

view this post on Zulip Mario Carneiro (Aug 09 2018 at 09:30):

if you assume archimedean A and discrete_linear_ordered_field A, then you can prove that rat.cast is a dense embedding by just generalizing the existing proof dense_embedding_of_rat, and hence define a function like real.cast out of A

view this post on Zulip Mario Carneiro (Aug 09 2018 at 09:31):

and then you have your isomorphism

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 09:59):

Kevin: https://en.wikipedia.org/wiki/Real_number#%22The_complete_ordered_field%22

Oh thanks for this Patrick! That clears this mess up!

view this post on Zulip Patrick Massot (Aug 09 2018 at 10:00):

Remember: if it's not formalized, you don't even know what you are talking about.

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 10:36):

this is a fabulous example of this! I was talking to Chris about this last week and just ended up confused. I said "did you know that the reals are the unique complete ordered field?" and he replied "don't you need some archimedean property" and I said "oh yeah, what happens if you adjoin an infinitesimal?" and it was at this point that I realised I was no longer quite sure what I was talking about.

view this post on Zulip Mario Carneiro (Aug 09 2018 at 10:45):

what is an example of a complete nonarchimedean field?

view this post on Zulip Johan Commelin (Aug 09 2018 at 10:45):

Q_p

view this post on Zulip Mario Carneiro (Aug 09 2018 at 10:45):

ordered field?

view this post on Zulip Johan Commelin (Aug 09 2018 at 10:45):

Hmmm. Don't know about those.

view this post on Zulip Mario Carneiro (Aug 09 2018 at 10:46):

In my proof sketch, you definitely need archimedean to prove dense embedding, but I think you can use completeness to prove archimedean

view this post on Zulip Johan Commelin (Aug 09 2018 at 10:46):

Seems reasonable

view this post on Zulip Mario Carneiro (Aug 09 2018 at 10:47):

If completeness means dedekind-complete, then the sup of N is contradictory so you get archimedean that way

view this post on Zulip Mario Carneiro (Aug 09 2018 at 10:48):

but if it is only complete relative to the uniformity it's not obvious to me

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 10:49):

I am in the middle of something else at the minute but I convinced myself last week that you could put an order on R(ϵ)\mathbb{R}(\epsilon) with ϵ\epsilon smaller than any positive real but greater than zero. Can one complete this, for some notion of completion?

view this post on Zulip Mario Carneiro (Aug 09 2018 at 10:50):

wait, Q_p isn't nonarchimedean

view this post on Zulip Mario Carneiro (Aug 09 2018 at 10:50):

it isn't ordered so the term doesn't apply

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 10:50):

It is for some definition

view this post on Zulip Rob Lewis (Aug 09 2018 at 10:50):

It has a nonarchimedean norm.

view this post on Zulip Johan Commelin (Aug 09 2018 at 10:50):

What the hack does "nonarchimedean" mean if even Q_p is no longer an example.... (shakes head...)

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 10:51):

I have a book called "nonarchimedean analysis" which defines a nonarchimedean field to be a field complete with respect to a non-trivial nonarchimedean norm.

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 10:51):

and a nonarchimedean norm is a function from the field to the non-negative reals satisfying F(x)=0 iff x=0, F(xy)=F(x)F(y) and F(x+y)<=max(F(x),F(y))

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 10:51):

and non-trivial means "not the one with F(x)=1 for x non-zero and F(0)=0"

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 10:52):

and complete in this context means the underlying metric space is complete with d(x,y)=F(x-y)

view this post on Zulip Mario Carneiro (Aug 09 2018 at 10:52):

what does an archimedean norm have to do with the archimedean property? the definitions look completely different

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 10:53):

Oh sorry, I defined a nonarchimedean norm above, I'll edit

view this post on Zulip Mario Carneiro (Aug 09 2018 at 10:53):

wiki says a nonarchimedean norm is one that defines an ultrametric, but I don't see what that has to do with 1+1+1+...

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 10:54):

A norm is F as above but with F(x+y)<=max(F(x),F(y)) weakened to F(x+y)<=F(x)+F(y)

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 10:54):

and a norm is defined to be archimedean if it is not nonarchimedean (seriously)

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 10:55):

I think the two uses of archimedean are unfortunate, and are probably just related to the fact that the reals satisfies both properties

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 10:55):

As Patrick says, if you haven't formalised it, you don't know what you're talking about

view this post on Zulip Mario Carneiro (Aug 09 2018 at 10:56):

I want to call that an ultranorm, it makes more sense

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 10:56):

What would you like my book to be called?

view this post on Zulip Mario Carneiro (Aug 09 2018 at 10:56):

ultra analysis?

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 10:57):

I think it would have sold more copies with that title

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 10:57):

Bosch--Guentzer--Remmert

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 10:57):

It's a classic. I read it from cover to cover.

view this post on Zulip Mario Carneiro (Aug 09 2018 at 10:58):

anyway, which of these archimedeans is the one we care about?

view this post on Zulip Johan Commelin (Aug 09 2018 at 10:59):

Number theorists care about the normy version.

view this post on Zulip Mario Carneiro (Aug 09 2018 at 10:59):

I mean for uniqueness of R

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 11:00):

Did you see Patrick's Wikipedia link? That says something about the confusion. But the definition of an archimedean norm is, I believe, nothing to do with the uniqueness statement about the reals.

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 11:01):

The only role I've ever seen that "archimedean = not non-archimedean" definition play is when classifying all norms on number fields. I am honestly not sure it's used anywhere else.

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 11:02):

Maybe in Cassels' "Local Fields" there'a a section on archimedean norms, and it might even say that every field with an archimedean norm is a subfield of the complexes or something.

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 11:03):

I forget the lemma. Certainly the theorem is that the archimedean norms on a number field are all induced from embeddings into the complexes (modulo some equivalence relation on norms which is "induced metrics define the same topology")

view this post on Zulip Mario Carneiro (Aug 09 2018 at 11:04):

wait, so does R have any uniqueness property that does not reference the order?

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 11:07):

The complexes are the unique algebraically closed field of characteristic zero and cardinality 2^aleph_0 (proof: transcendence basic; probably I'm assuming AC here). If you take an element of order 2 in Aut(complexes) then its fixed points are a field which I think is not in general isomorphic to the reals but which is quite difficult to tell apart from the reals if you don't think about the ordering.

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 11:08):

Hmm, maybe the fixed points do even have an ordering, perhaps it's this unboundedness of 1+1+1+... which fails in these general fields (are they called "real closed fields"?)

view this post on Zulip Mario Carneiro (Aug 09 2018 at 11:08):

If you allow the topology, you should be able to get R exactly, right?

view this post on Zulip Mario Carneiro (Aug 09 2018 at 11:08):

there is only one nontrivial continuous automorphism of C

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 11:08):

right

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 11:09):

but I defined it as an abstract field

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 11:09):

Take Q, adjoin 2^aleph_0 independent transcendental elements, and then take the alg closure

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 11:09):

This proves that C is isomorphic to an algebraic closure of Q_p

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 11:10):

and an algebraic closure of Q_p has a non-archimedean norm on it, which makes it a metric space, and this metric space is not complete, and if you complete it then you get something called C_p, which by the same argument is also isomorphic to C

view this post on Zulip Mario Carneiro (Aug 09 2018 at 11:10):

isomorphic as fields?

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 11:10):

So there's lots of different topologies on C

view this post on Zulip Johan Commelin (Aug 09 2018 at 11:11):

isomorphic as fields?

yes

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 11:11):

Yes, any two alg closed fields of char 0 and cardinality 2^aleph_0 are isomorphic

view this post on Zulip Mario Carneiro (Aug 09 2018 at 11:11):

but if you want to capture "complete" from the original statement, you want a topological field structure

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 11:11):

Proof is "take a transcendence basis over Q, check it has size 2^aleph_0, hence your field must be iso to an alg closure of Q(X_i:i in reals)

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 11:13):

So if c is a random automorphism of order 2 of (alg closure of Q(X_i : i in reals)) then I think you can define an order on the fixed subfield, by x > 0 iff x is a non-zero square

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 11:14):

but before I say too much more I should look at the Wikipedia article on real closed fields and I'm trying to read a student's work on homotopy theory :-/

view this post on Zulip Johan Commelin (Aug 09 2018 at 11:23):

I think real closed fields would be a really cool topic to formalise as well.

view this post on Zulip Johan Commelin (Aug 09 2018 at 11:23):

There is lots of interesting logic there.

view this post on Zulip Johan Commelin (Aug 09 2018 at 11:24):

Quantifier elimination. Semialgebraic sets. https://en.wikipedia.org/wiki/Cylindrical_algebraic_decomposition

view this post on Zulip Johan Commelin (Aug 09 2018 at 11:25):

Anyway, I'm derailing this topic.

view this post on Zulip Kenny Lau (Aug 09 2018 at 13:25):

there is an order on Q_p

view this post on Zulip Kenny Lau (Aug 09 2018 at 13:26):

wait the order isn't compatible with the ring structure


Last updated: May 10 2021 at 07:15 UTC