Real Closed Fields

Stream: maths

[Aaron Anderson]

I've started a branch mathlib:rcf for defining and proving things about real closed fields.

[Aaron Anderson]

I've proven some basics that could use golfing, and provided a lot of sorries. I invite any help closing those sorries or adding new relevant ones.

[Aaron Anderson]

@Adam Topaz

[Aaron Anderson]

Unfounded optimism alert: most of the exciting sorries probably actually need Galois theory

[Aaron Anderson]

I’d wager there’s still at least one PR to be made before then though

[Adam Topaz]

@Aaron Anderson Great! One note: your statement of Artin-Shreier is wrong. You need K|k to a finite extension and of degree greater than 1.

[Adam Topaz]

I think the first two sorry's should definitely be doable now. It's just the fact that a quadratic monic polynomial over a field is irreducible if and only if it has no root. Does mathlib have this?

[Johan Commelin]

@Jack J Garzella you were working on quadratic monics, right?

[Johan Commelin]

@Aaron Anderson I'm excited about this, but atm don't have time to contribute... sorry.

[Adam Topaz]

@Aaron Anderson @Johan Commelin I also think it would be very exciting to have Artin-Schreier. It's the "first" theorem in anabelian geometry (of course, to state it in a proper anabelian way one needs to speak about absolute Galois groups hence about profinite groups, which seems to be a long ways away).

[Johan Commelin]

"Long" is a relative notion if you get @Kenny Lau interested (-;

[Aaron Anderson]

I’m not sure it’s as simple as just showing which monics and quadratics are irreducible... we can show that any other irreducible polynomial has even degree greater than 3. If we have a large even-degree extension, then with Galois theory and Sylow, we can produce a sub-extension of degree 2, but it’s slipping my mind how else we can reduce that to quadratic extensions.

[Adam Topaz]

You're right about the second sorry, but the first one is easier

[Adam Topaz]

A square root of -1 contradicts the existence of an order

[Jack J Garzella]

@Adam Topaz @Johan Commelin I have an outline for the proof that a quadratic monic polynomial is reducible if it has a root, with a few sorries.

[Jack J Garzella]

Unfortunately I don’t have time to work on this until after the first week of September. If you want I can share my code

[Adam Topaz]

I will also be busy for the next few weeks, but it would be great if you share your code anyway :grinning_face_with_smiling_eyes:. Is it on a branch of mathlib?

[Jack J Garzella]

Indeed it is on a branch: https://github.com/jjgarzella/mathlib/tree/split_degree_two, note that the mathlib is a few weeks old at this point