Real Closed Fields Project

Stream: mathlib4

[Artie Khovanov]

I'm formalising some real algebra in Mathlib :slight_smile:
https://artie2000.github.io/real_closed_field/
I've got a blueprint, which should make it relatively easy to contribute if you are interested!
I've already formalised some material on orderings of rings and fields.
I think a good target is the characterisation of real closed fields (Theorem 40 / RCF_tfae).
I have some material beyond this (Sturm's theorem, real closures, Artin-Schreier theorem) but I haven't fully worked out a path to formalising it.
Eventually I want to prove the Tarski-Seidenberg principle, but that's quite far away and I'm not really sure how equipped Lean is to handle the computational aspects of the theory.
I'm doing this in my spare time, so progress will be slow, but any contributions are very welcome! The ultimate goal is to upstream everything to Mathlib.

[Kenny Lau]

wow that's quite quick!

[Violeta Hernández]

Hi! I'm interested in this. I kind of need this in order to show surreals are real closed.

[Artie Khovanov]

@Violeta Hernández what results do you need? See the blueprint for what I have planned

[Violeta Hernández]

I need the result that for $R$ a real-closed field and $\Gamma$ a divisible group, the field of Hahn series $R[[X^\Gamma]]$ is also real-closed

[Violeta Hernández]

I'm not really sure if this is more of a Hahn series result or a real-closed field result

[Violeta Hernández]

Found this on ncatlab
image.png

[Artie Khovanov]

Yep OK so the only bit of real closed field theory you need there is that index 2 in algebraic closure implies real closed (so, Theorem 50 in the current version of my blueprint)

[Artie Khovanov]

The rest is Hahn series stuff eg k[t^G][i]=k[i][t^G]

[Artie Khovanov]

At the moment that result (Theorem 50) is a while away, at least the way I want to prove it, due to missing API around quadratic extensions (see Lemma 3)
But any contributions in this direction would of course be very welcome :)

[Violeta Hernández]

How do you even write down K[i] in Mathlib?

[Artie Khovanov]

AdjoinRoot K (X^2 + 1)

[Artie Khovanov]

And, if you already have your field, use IsAdjoinRoot

[Violeta Hernández]

Thanks!

[Violeta Hernández]

I'll read about this. Hope I'm not jumping into something far beyond my depth...

[Artie Khovanov]

Nothing in the blueprint is really beyond the level of a first course in number fields, if you take the ordering stuff as given
And much of the proofs is just polynomial manipulation
I'm still getting to grips with this part of the library though; it feels like there's definitely missing API

[Violeta Hernández]

Polynomials in Mathlib my beloathed

[Artie Khovanov]

There isn't even a normal form for them

[Weiyi Wang]

I reminded myself about this project as I stumbled upon some theory mentioning real-closeness. Specifically this lemma: a Gamma-valued, real-closed or algebraically closed field F has a section (a group homomorphism Gamma->F that's right inverse of the valuation. I wonder if it is in the scope of the project, or when the definition of real closed field will be ready in mathlib to express this.

[Aaron Liu]

for any Gamma?

[Aaron Liu]

or does the valuation have to be surjective

[Aaron Liu]

wait what do you mean the field has a section, and where did the valuation come from

[Weiyi Wang]

For any valuation. Gamma just refers to the value group (so surjectivity implied). "Section" is just name given to the homomorphism in the article I am reading

[Artie Khovanov]

I have "real closed field" stated but I haven't proved much about them yet
the API around finite extensions of fields needs work

[Weiyi Wang]

:smile: Would be nice to see it in mathlib even with just simple definition and lemmas. I think the actual lemma I need is "you can take n-th root in real closed fields"

[Artie Khovanov]

Well, you can't take nth roots, necessarily. You can take them when n is odd, or when n is even and your element is non-negative. Stuff about real closed fields is generally proved from the algebraically closed field version using the characterisation of real closed fields as non-algebraically-closed fields whose extension by $\sqrt{-1}$ is algebraically closed.

[Weiyi Wang]

sorry I should clarify I meant taking n-th root of a positive number

[Artie Khovanov]

Here is the definition I have right now:

/- An ordered field is real closed if every nonegative element is a square and
   every odd-degree polynomial has a root. -/
class IsRealClosed (R : Type*) [Field R] [LinearOrder R] : Prop extends IsStrictOrderedRing R where
  isSquare_of_nonneg {x : R} (hx : 0 ≤ x) : IsSquare x
  exists_isRoot_of_odd_natDegree {f : R[X]} (hf : Odd f.natDegree) : ∃ x, f.IsRoot x

I don't have much else (you can check out the project blueprint to see current scope and progress)

[Violeta Hernández]

I'd love to see the definition in Mathlib too. That way I can add the relevant proof_wanted for my project!

[Filippo A. E. Nuccio]

I think @Florent Schaffhauser had somethink on this.

[Artie Khovanov]

Yes, this project comes as a result of his work on real algebra.