RealCast

Stream: mathlib4

[Violeta Hernández]

A monoid (with one) admits an embedding from $\mathbb N$. A group (with one) admits an embedding from $\mathbb Z$. A division ring admits an embedding from $\mathbb Q$. Is there any nice characterization for structures that admit an embedding from $\mathbb R$?

[Violeta Hernández]

The obvious answer is "archimedean linearly ordered division rings" but it's a pretty lame answer, since any such field is isomorphic to the reals. I'm rather thinking about structures like the hyperreals, or surreal numbers, or real rational functions.

[Aaron Liu]

Violeta Hernández said:

The obvious answer is "archimedean linearly ordered division rings" but it's a pretty lame answer, since any such field is isomorphic to the reals.

pretty sure this part is wrong

[Violeta Hernández]

might need to strengthen that to field

[Aaron Liu]

for example, the rationals are an Archimedean linearly ordered division ring which does not admit an embedding from the reals

[Violeta Hernández]

Ah, you're right

[Aaron Liu]

Violeta Hernández said:

might need to strengthen that to field

Rationals are also a field

[Violeta Hernández]

"Conditionally complete" is the missing adjective

[Michael Stoll]

Violeta Hernández said:

A monoid (with one) admits an embedding from $\mathbb N$. A group (with one) admits an embedding from $\mathbb Z$. A division ring admits an embedding from $\mathbb Q$.

This is not actually true; you need something like "characteristic zero" to get an embedding (and to get a map at all in the $\mathbb Q$ case).

[Violeta Hernández]

The reason I want this is because of a result about non-archimedean fields: if you have a ring with a strictly monotone map f : ℝ ->+* K, and given x y : K in the same docs#ArchimedeanClass, there's a unique r : ℝ such that x - r * y is in a higher ArchimedeanClass (i.e. is infinitesimal compared to x and y).

[Violeta Hernández]

I was wondering if there was any set of hypotheses that would uniquely specify the map f, rather than having to pass it around everywhere

[Michael Stoll]

Aren't there lots of (order-preserving) embeddings of $\mathbb R$ into the surreals?

[Kenny Lau]

do you just say map pi to pi+ε (while fixing Q)?

[Aaron Liu]

Violeta Hernández said:

I was wondering if there was any set of hypotheses that would uniquely specify the map f, rather than having to pass it around everywhere

There is no such uniqueness by model theory stuff probably

[Aaron Liu]

not if your hypotheses are invariant under ordered field isomorphism

[Michael Stoll]

Kenny Lau said:

do you just say map pi to pi+ε (while fixing Q)?

Roughly. You fix a transcendence basis of $\mathbb R$ over $\mathbb Q$ and move the standard images infinitesimally.

[Violeta Hernández]

Michael Stoll said:

Aren't there lots of (order-preserving) embeddings of $\mathbb R$ into the surreals?

Order embedding yes, but addition and multiplication preserving as well?

[Aaron Liu]

For any two surreals transcendental over the rationals which are in the same dedekind cut, you can find an ordered field automorphism of the surreals sending one to the other

[Michael Stoll]

I think so; see above: given the images of a transcendence basis, you can uniquely extend to a field hom, and the images will still be infinitesimally close to the standard ones.

[Kenny Lau]

Violeta Hernández said:

Michael Stoll said:

Aren't there lots of (order-preserving) embeddings of $\mathbb R$ into the surreals?

Order embedding yes, but addition and multiplication preserving as well?

you can't find a contradiction if I fix Q but map pi to pi+ε (in my example above)

[Kenny Lau]

because pi is transcendental

[Violeta Hernández]

Ah, shucks. I guess you do need the extra birthday structure in order to make the map from reals to surreals canonical.

[Aaron Liu]

Aaron Liu said:

For any two surreals transcendental over the rationals which are in the same dedekind cut, you can find an ordered field automorphism of the surreals sending one to the other

I've heard this result over and over but now I'm not so sure I have to double check

[Violeta Hernández]

It feels correct

[Violeta Hernández]

Does the argument of "take a transcendental basis and tweak it infinitesimally" not work?

[Aaron Liu]

For example, surely sqrt2+epsilon and sqrt2-epsilon are distinguishable?

[Aaron Liu]

They don't seem to satisfy any polynomial equation

[Aaron Liu]

And they're ordered the same wrt all the rationals

[Aaron Liu]

But one is larger than every square root of two and the other one is not

[Michael Stoll]

$\sqrt{2}$ is not transcendental. All algebraic real numbers have to stay put!

[Kenny Lau]

aha, it's ∃ y, y ^ 4 = 2 ∧ ∃ z, x = y * y + z * z that is satisfied by x = sqrt2+epsilon but not x = sqrt2-epsilon

[Kenny Lau]

(in words: x is greater than the positive square root of 2, "greater than" is encoded by z, the positive square root of 2 is encoded by y * y)

[Alex Meiburg]

I mean every level of the https://en.wikipedia.org/wiki/Cayley%E2%80%93Dickson_construction would admit a RealCast

[Alex Meiburg]

But, I don't think any of those except Complex and Quaternion are in Mathlib.

[Violeta Hernández]

I guess there's a separate question that's worth asking: should we have a typeclass for types with a "canonical" embedding from ℝ?

[Alex Meiburg]

Similarly, an algebra over a RealCast inherits a RealCast. (Which I guess includes those two, but also e.g. Polynomial[\bbR].)
Also, docs#Hyperreal, and Hypercomplex (not in mathlib) would get one.

[Alex Meiburg]

Violeta Hernández said:

should we have a typeclass for types with a "canonical" embedding from ℝ

How is that different from RealCast? Does not the realcast function provide a "canonical" choice?

[Violeta Hernández]

Well, RealCast doesn't exist in Mathlib, is my point

[Alex Meiburg]

Well you said a "separate question", what's the first question?

[Violeta Hernández]

The first question was whether there existed some nice set of typeclasses that would imply some canonical embedding from ℝ

[Aaron Liu]

and the answer is I think "there's no such thing as a canonical embedding"

[Kenny Lau]

not even (Complex, norm)?

[Aaron Liu]

well there's no embedding which is natural for field homomorphisms

[Aaron Liu]

and there's no embedding which is natural for ordered field homomorphisms

[Aaron Liu]

so we need more than that

[Violeta Hernández]

Maybe the real answer here is "I should make an Algebra ℝ Surreal instance and work with that"

[Yakov Pechersky]

(Compact) Banach algebras?

[Artie Khovanov]

@Violeta Hernández I feel like the correct analogues here are surely embeddings from $\mathbb{R}_\text{alg}$ and then from $\mathbb{C}_\text{alg}$ (i.e. $\bar{\mathbb{Q}}$). These are, respectively, real closed and algebraically closed fields (along with a choice of root of every relevant rational polynomial).

[Artie Khovanov]

oh possibly the analogues of these objects for division rings, rather