Formally real fields

Stream: mathlib4

[Artie Khovanov]

Is there anything in Mathlib on the relationship between formally real fields [-1 not a sum of squares] and [linear] ordered fields? I see that a notion of positive cones has been defined for groups and rings; is there anything more?

(I think this notion can be extended to formally real rings, I could implement that too if people want)

[Kim Morrison]

I don't think there is. Sounds reasonable!

[Riccardo Brasca]

We already have the notion of formally real field. cc @Flo (Florent Schaffhauser)

[Artie Khovanov]

Where is this defined? I can't find it from a quick search.

[Florent Schaffhauser]

Hi @Artie Khovanov :wave:

Sorry, I am not fully available these days. We had a repo on formally real fields here:

https://github.com/riccardobrasca/formally_real

And in Mathlib, we have the following:

• docs#IsSumSq
• docs#IsSemireal

The repo on @Riccardo Brasca 's GitHub contains a proof that a field is formally real iff it admits an ordering compatible with field structure (Artin-Schreier theory). Would you be interested in working jointly on getting this into mathlib? We could meet over Zoom to discuss this, or manage it via DM :smile:

[Yaël Dillies]

@Riccardo Brasca, it's good practice to include a licence in your repo so that we know we can PR stuff from it to Mathlib. Of course, we should also ask you first, but in the event of a really long beach enjoyment session on your part it's good to know that we can get those juicy positive cones in

[Floris van Doorn]

As an outsider looking at the definition of docs#IsSemireal, why have we included the condition that 0 ≠ 1? In any type where -0 = 0 holds, this follows from ¬IsSumSq (-1) and the definition of IsSumSq. And surely we don't care about types where -0 = 0 fails.

[Scott Carnahan]

I also find the definition of docs#IsSemireal a bit odd, for orthogonal reasons: we could replace ¬IsSumSq (-1 : R) with something like ¬∃ (x : R), IsSumSq x ∧ x + 1 = 0 and avoid [Neg R] altogether.

[Artie Khovanov]

I agree with both of these objections; I want to refactor the two files on cones and IsSemireal to make them easier to use and more general, as well as integrating the additional material on formally real fields.

[Artie Khovanov]

I generalised the IsSemireal file using @Floris van Doorn and @Scott Carnahan's suggestions. Here is my draft:
https://github.com/leanprover-community/mathlib4/commit/5fa28782c709f9db08987f052a348af91c9330f2
I welcome any feedback -- I will hopefully be building on this to integrate @Riccardo Brasca's work in the future.

[Johan Commelin]

Thanks, I left two comments on GH

[Artie Khovanov]

Have updated accordingly.

[Johan Commelin]

Is your code on some branch? (I don't know how to find your new commit)

[Artie Khovanov]

Oh sorry
It's the real-closed-field-dev branch:
https://github.com/leanprover-community/mathlib4/tree/real_closed_field_dev

[Artie Khovanov]

I want to replace the definition of sumSqIn with multiple definitions for the various structures (AddMonoid, Semiring, RingCone) called AddMonoid.sumSqIn etc.
@Riccardo Brasca I belive you were the one that made sumSqIn be defined as a monoid; will this change fundamentally break anything downstream? At worst I think this would require renaming some stuff, but I am inexperienced with the design of the library.

[Artie Khovanov]

By the way my PR rewriting positive cones is about to go live:
https://github.com/leanprover-community/mathlib4/pull/15975

[Eric Wieser]

I worry a little about how many new structures that PR introduces, because every new structure creates quite a big API burden. On the other hand, that doesn't mean that it's the wrong approach, just that we should have more machinery to make it more obviously the right approach!

[Artie Khovanov]

The new structures I have added are the multiplicative versions of the group cones, and also the cones with squares, which I will need for the formally real field stuff.

The other structures already existed, but I rewrote them to have a more standard definition and also to extend Submonoid and Subsemiring to make them easier to work with.

[Artie Khovanov]

By the way, what alternatives are there to structures in this sort of situation?

[Eric Wieser]

One option is to have fewer structures and more predicates; for instance, we don't have a structure for "injective linear maps", you have to pass the linear maps and Function.Injective separately

[Eric Wieser]

That's not to say this is a better choice in your situation

[Artie Khovanov]

Oh I see what you mean. Having predicates for the Maximal and WithSquares forms would be fine, I'm pretty indifferent.

[Artie Khovanov]

Should I refactor it to that? Or is it good as is?

[Artie Khovanov]

Artie Khovanov said:

I want to replace the definition of sumSqIn with multiple definitions for the various structures (AddMonoid, Semiring, RingCone) called AddMonoid.sumSqIn etc.
Riccardo Brasca I belive you were the one that made sumSqIn be defined as a monoid; will this change fundamentally break anything downstream? At worst I think this would require renaming some stuff, but I am inexperienced with the design of the library.

Update: a draft of my additions is available at
https://github.com/leanprover-community/mathlib4/blob/real_closed_field_dev/Mathlib/Algebra/Ring/SumsOfSquares.lean
(Compare: https://github.com/leanprover-community/mathlib4/compare/real_closed_field_dev)

[Artie Khovanov]

Update: here is my PR
https://github.com/leanprover-community/mathlib4/pull/16094

[Johan Commelin]

Note that you can simply write #16094. (For some value of simply.)

[Johan Commelin]

@Artie Khovanov please update the title of the PR to follow the commit guidelines: https://leanprover-community.github.io/contribute/commit.html

[Artie Khovanov]

Have now changed the title

[Artie Khovanov]

My branches have silly names but that's because I made them before Yael convinced me to use a sane workflow.