## Stream: maths

### Topic: reals are unique complete ordered field

#### 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 :-)

#### Mario Carneiro (Aug 09 2018 at 08:56):

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

#### Mario Carneiro (Aug 09 2018 at 08:57):

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

#### 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

#### 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

#### Mario Carneiro (Aug 09 2018 at 09:00):

That's often true

#### Mario Carneiro (Aug 09 2018 at 09:01):

concrete constructions have the drawback that lean can start unfolding them

#### 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?

#### Johan Commelin (Aug 09 2018 at 09:16):

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

#### Mario Carneiro (Aug 09 2018 at 09:17):

heh, I guess I did

#### 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?

#### Mario Carneiro (Aug 09 2018 at 09:18):

It is under more assumptions

#### Mario Carneiro (Aug 09 2018 at 09:18):

extend_eq requires that the space be t2

#### Mario Carneiro (Aug 09 2018 at 09:18):

and tendsto_extend needs that it is regular

#### Mario Carneiro (Aug 09 2018 at 09:18):

I guess Q is not a regular space?

#### Johan Commelin (Aug 09 2018 at 09:18):

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

#### Johan Commelin (Aug 09 2018 at 09:19):

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

#### Mario Carneiro (Aug 09 2018 at 09:19):

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

#### 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).

#### Mario Carneiro (Aug 09 2018 at 09:21):

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

#### 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))


#### 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

#### 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

#### Mario Carneiro (Aug 09 2018 at 09:31):

and then you have your isomorphism

#### Kevin Buzzard (Aug 09 2018 at 09:59):

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

#### Patrick Massot (Aug 09 2018 at 10:00):

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

#### 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.

#### Mario Carneiro (Aug 09 2018 at 10:45):

what is an example of a complete nonarchimedean field?

Q_p

ordered field?

#### 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

Seems reasonable

#### 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

#### Mario Carneiro (Aug 09 2018 at 10:48):

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

#### 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 $\mathbb{R}(\epsilon)$ with $\epsilon$ smaller than any positive real but greater than zero. Can one complete this, for some notion of completion?

#### Mario Carneiro (Aug 09 2018 at 10:50):

wait, Q_p isn't nonarchimedean

#### Mario Carneiro (Aug 09 2018 at 10:50):

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

#### Kevin Buzzard (Aug 09 2018 at 10:50):

It is for some definition

#### Rob Lewis (Aug 09 2018 at 10:50):

It has a nonarchimedean norm.

#### 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...)

#### 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.

#### 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))

#### 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"

#### 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)

#### 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

#### Kevin Buzzard (Aug 09 2018 at 10:53):

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

#### 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+...

#### 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)

#### Kevin Buzzard (Aug 09 2018 at 10:54):

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

#### 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

#### 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

#### Mario Carneiro (Aug 09 2018 at 10:56):

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

#### Kevin Buzzard (Aug 09 2018 at 10:56):

What would you like my book to be called?

ultra analysis?

#### Kevin Buzzard (Aug 09 2018 at 10:57):

I think it would have sold more copies with that title

#### Kevin Buzzard (Aug 09 2018 at 10:57):

Bosch--Guentzer--Remmert

#### Kevin Buzzard (Aug 09 2018 at 10:57):

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

#### Mario Carneiro (Aug 09 2018 at 10:58):

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

#### Johan Commelin (Aug 09 2018 at 10:59):

Number theorists care about the normy version.

#### Mario Carneiro (Aug 09 2018 at 10:59):

I mean for uniqueness of R

#### 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.

#### 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.

#### 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.

#### 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")

#### Mario Carneiro (Aug 09 2018 at 11:04):

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

#### 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.

#### 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"?)

#### Mario Carneiro (Aug 09 2018 at 11:08):

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

#### Mario Carneiro (Aug 09 2018 at 11:08):

there is only one nontrivial continuous automorphism of C

right

#### Kevin Buzzard (Aug 09 2018 at 11:09):

but I defined it as an abstract field

#### Kevin Buzzard (Aug 09 2018 at 11:09):

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

#### Kevin Buzzard (Aug 09 2018 at 11:09):

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

#### 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

#### Mario Carneiro (Aug 09 2018 at 11:10):

isomorphic as fields?

#### Kevin Buzzard (Aug 09 2018 at 11:10):

So there's lots of different topologies on C

#### Johan Commelin (Aug 09 2018 at 11:11):

isomorphic as fields?

yes

#### Kevin Buzzard (Aug 09 2018 at 11:11):

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

#### 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

#### 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)

#### 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

#### 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 :-/

#### Johan Commelin (Aug 09 2018 at 11:23):

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

#### Johan Commelin (Aug 09 2018 at 11:23):

There is lots of interesting logic there.

#### Johan Commelin (Aug 09 2018 at 11:24):

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

#### Johan Commelin (Aug 09 2018 at 11:25):

Anyway, I'm derailing this topic.

#### Kenny Lau (Aug 09 2018 at 13:25):

there is an order on Q_p

#### 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