real closed field in mathlib?

Stream: mathlib4

[Jihoon Hyun]

Is there real closed field defined in mathlib? Not that I have a deep understanding on the subject, but I just got curious.

[Yaël Dillies]

No we don't have them. @Artem Khovanov expressed interest in porting their formalisation of Puiseux series from Isabelle to Lean

[Jihoon Hyun]

Actually, defining the real (closed) field itself should be easy, according to Real Algebraic Geometry by Bochnak, Coste, and Roy. It takes only three pages (7, 8, 9) introducing the necessary definitions to define it. So it really seems like anyone (including me) can try to 'only define' it..

[Artie Khovanov]

Yeah, specifically I want to formalise Thom encoding and also that Puiseux series over an RCF form an RCF. Going to have some time this summer to do this. Would be very happy to collaborate on this, especially because my Lean skills are not that good!

[Jihoon Hyun]

I struggled a bit reading the book, but it seems like RealClosedField is just

class RealClosedField (F : Type u) extends LinearOrderedField F where
  no_nontrivial_real_algebraic_extension (L : Type u) [LinearOrderedField L] [Algebra L F] : L = F

It should be correct if Algebra L F implies the field extension L/F.

[Artie Khovanov]

Strictly speaking, you also need to specify that the ordering on the extension extends the ordering on your original field. However, this definition is equivalent, since an RCF can be characterised as "an ordered field of index 2 in its own algebraic closure", and algebraically closed fields can never be ordered.

There are about 4 equivalent definitions of RCF sthat are useful in different contexts; I'd say proving their equivalence is one of the important things to do, for my purposes.

I think the most concrete/useful definition is the one that says roots of odd-degree polynomials and square roots of positive elements both exist.

[Jihoon Hyun]

Then I'll set proving those equivalences as the first goal. But you should keep in mind that I'm new to this subject..

[Michael Stoll]

Jihoon Hyun said:

It should be correct if Algebra L F implies the field extension L/F.

Algebra does not imply that the extension is algebraic, though. (There are transcendental real-closed extensions of the reals, I would think.)

[Jihoon Hyun]

Thanks for notifying @Michael Stoll ! With additional search I could find Algebra.IsAlgebraic, and I guess this is the right thing to use?

[Luigi Massacci]

Where do you plan to work on this? I'd be interested in contributing

[Jihoon Hyun]

class RealClosedField (F : Type u) extends LinearOrderedField F where
  no_nontrivial_real_algebraic_extension (L : Type u) [LinearOrderedField L] [Algebra L F] [Algebra.IsAlgebraic L F] : L = F

[Michael Stoll]

docs#Algebra.IsAlgebraic (this produces a link to the declaration in the Mathlib documentation) -- yes, this looks like it should be the correct condition.

[Jihoon Hyun]

@Luigi Massacci We just started (at least in my perspective), and nothing is set up (also in my perspective), yet. Since I'm new to this subject, it is likely that those who know real algebraic geometry well should manage the project. But if you don't mind, I'd be happy to create a repository for this.

[Adam Topaz]

Don't you need to assume the field extension is compatible with the ordering?

[Luigi Massacci]

Yes, if you create a fork of mathlib that would be cool. Unfortunately I won't be able to help until the 21st (exams :( but if you still have stuff left to do by then I'll jump in

[Adam Topaz]

Also using equality between L and F is not what you want. Rather you would want to say that the map F -> L is an isomorphism.

[Adam Topaz]

If you ask me, I would say that real closed fields should be defined in terms of saying that any positive element has a square root and any odd degree polynomial has a root.

[Adam Topaz]

Or by assuming the intermediate value theorem for polynomials.

[Johan Commelin]

Yes, I think the definition should be the first order logic version of the four equivalent defs that Artie was talking about. The other 3 should be both consequences and alternative constructors.

[Riccardo Brasca]

@Flo (Florent Schaffhauser) is interested in this I think

[Jihoon Hyun]

How do you think about this formulation? The second prop which I believe everyone is talking about looks ugly as I couldn't find a better way to denote a unique ordering.

theorem real_closed_tfae {F : Type*} [Field F] : List.TFAE [
  [LinearOrderedField F] → (K : Type u) → [LinearOrderedField K] → [Algebra K F] → [Algebra.IsAlgebraic K F]
    → (φ : F →+* K) → (∀ f₁ f₂, f₁ ≤ f₂ → φ f₁ ≤ φ f₂) → Function.Bijective φ,
  ∃! (ord : F → F → Prop), (∀ x y, ord x y → ∀ z, ord (z + x) (z + y)) ∧ (∀ x y, ord 0 x → ord 0 y → ord 0 (x * y))
    ∧ (fun x => ord 0 x : Set F) = (fun x => ∃ y, x = y * y)
    ∧ (∀ p : Polynomial F, Odd p.degree → ∃ r, r ∈ p.roots),
  (K : Type u) → [Field K] → [Algebra F K] → [IsCyclotomicExtension {2} F K] → IsAlgClosed K
  ] := sorry

[Artie Khovanov]

Adam Topaz said:

Don't you need to assume the field extension is compatible with the ordering?

It's an equivalent condition (but ofc it's better to include this assumption).

[Adam Topaz]

Equivalent in what sense?

[Adam Topaz]

It’s certainly not true that a field theoretic embedding of ordered fields is an ordered embedding. For example $\mathbb{Q}(t)$ has many nonisomorphic field orderings.

[Adam Topaz]

Of course I understand that if $K$ is real closed then the only proper algebraic extension is $K[\sqrt{-1}]$ which can’t be ordered, so you can deduce that some condition is equivalent to the characterization of RCF, but this feels very circular.

[Artie Khovanov]

Adam Topaz said:

Of course I understand that if $K$ is real closed then the only proper algebraic extension is $K[\sqrt{-1}]$ which can’t be ordered, so you can deduce that some condition is equivalent to the characterization of RCF, but this feels very circular.

Yes, this is what I meant. I agree it would not be a sensible definition. Maybe I should have said "turns out to be equivalent".

[Adam Topaz]

Oh I just saw your earlier message Artie. Yes I agree with all that as well :)

[Adam Topaz]

Related to all of this, I would be very happy to see a proof of the Artin-Schreier theorem in mathlib (as well as its p-adic analog)

[Artie Khovanov]

Hi, an update -- I've started work on this now; the first thing I'm doing is making sure we have all the material on formally real fields. Once I am a little more established I will make a GitHub project for others to contribute. Apologies for the delay in getting this going!

[Riccardo Brasca]

You should really coordinate with @Flo (Florent Schaffhauser) (he may be on vacation now). We did quite a lot of stuff last year during the Leiden conference.

[Riccardo Brasca]

Ah you are talking about real closed field, not formally real. Sorry

[Artie Khovanov]

Riccardo Brasca said:

You should really coordinate with Flo (Florent Schaffhauser) (he may be on vacation now). We did quite a lot of stuff last year during the Leiden conference.

Well, I want to make sure all the stuff about formally real fields is there first, because it's needed for eg equivalent definitions of RCF. I've DMed Flo already, so hopefully we will collaborate on that.

[Artie Khovanov]

Here is the GitHub project:
https://github.com/FM22/real_closed_field
Please DM me to be added as a collaborator.