Real-closed Hahn series

Stream: maths

[Violeta Hernández]

I'm wondering how far we are from the following result: a Hahn series K[[T^Γ]] where K is real-closed and Γ is divisible is also real-closed. This result is relevant to me since it shows that surreal numbers (which are isomorphic to real Hahn series over themselves) are a real-closed field.

[Yaël Dillies]

cc @Artie Khovanov who has thought about that

[Artie Khovanov]

I have proved a slightly weaker result - Puiseaux rather than Hahn series - in Isabelle by generalising the analogous proof over ACFs. The proof is fairly elementary, progressively generalising Hensel's Lemma for power series by coordinate transformations. This makes it attractive for formalisation.

I have been working towards the theory of RCFs in Lean, but I haven't really done much since the Autumn. I wanted to do it properly, developing some real algebra etc first, but got a bit lost in scope creep (eg Mathlib is missing basic results on sums of squares).

You don't really need any RCF / Artin-Schreier theory for your result, of course - as long as you choose the right definition of an RCF ;)
I'd be happy to provide you a sketch of my argument and my references -- as far as I know, the RCF version is not published anywhere. Probably you can mine my proof to get to whatever version you need.

[Violeta Hernández]

What would the correct definition of an RCF be? In truth I don't think I'm looking for any particular definition of an RCF, since this result is likely to be a leaf result.

[Violeta Hernández]

References would be quite welcome, since I'm not very familiar with this part of algebra.

[Artie Khovanov]

Here are 4 characterisations of an RCF:
(1) Ordered field in which every positive element has a square root and every odd-degree polynomial has a root
(2) Ordered field satisfying the Intermediate Value Property for polynomials
(3) Ordered field maximal among algebraic extensions of ordered fields
(4) Model of Th(\bbR) in the language of ordered fields

(1) is the most hands on for algebraic stuff, and the one you'll want, but quite artificial
(2) is the best for developing "algebraic analysis" but also a bit artificial
(3) is more conceptual, it's what I would say an RCF "is" but I'm not an expert
(4) is cool and really strong

Proving equivalence of (1),(2),(3) is well within the scope of my Lean work; proving they imply (4) requires the Sturm-Tarski QE stuff and I think we are miles away from it.

[Violeta Hernández]

Any of the first three would be pretty great.

[Artie Khovanov]

OK I found the result I generalised to, it's pretty cursed:
image.png

[Artie Khovanov]

This result is taken from mining the proof of the Newton-Puiseaux theorem given by Shreeram S. Abhyankar in Algebraic Geometry for Scientists and Engineers (pp. 92 - 94).
You can actually read it on Google Books: https://books.google.co.uk/books?id=14LyBwAAQBAJ&pg=PA92

[Artie Khovanov]

With this result, let $K$ be an RCF -- characterisation (1). Then

• You can find a root of an odd-degree polynomial over $K\langle\!\!\!\langle X\rangle\!\!\!\rangle$ by applying the corollary by induction on degree.

• You can obtain a root of $X^2-f$, where $f>0$, by lifting a root of $X^2-a$, where $a>0$ is the leading coefficient of $f$, using part (2) of the theorem.

[Artie Khovanov]

The source is the following slides:
cambridge_talk.pdf
From the following talk:
https://www.youtube.com/watch?v=HBPg-K9ieng
(The talk isn't focused on the maths unfortunately)

[Violeta Hernández]

I'll give this a watch in the coming days

[Artie Khovanov]

Fair warning you won't come away understanding the maths any better

[Artie Khovanov]

Best source for that is probably the Abhyanar book
Oh yeah also note that I don't know how to generalise from Puiseaux to Hahn series
Or even if the argument I gave above does generalise
It probably does

[Antoine Chambert-Loir]

To your list of criteria for being a RCF, you could add
(5) -1 is not a square and R(sqrt (-1)) is algebraically closed,
which will allow to use the theorem that over an ACF, the field of Hahn series for a divisible group is also algebraically closed.

[Artie Khovanov]

Oh yeah you can do that as well, good idea! Although yeah you can also generalise the proof directly, as I did