Zulip Chat Archive

Stream: maths

Topic: Real Closed Fields


Aaron Anderson (Aug 15 2020 at 05:31):

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

Aaron Anderson (Aug 15 2020 at 05:33):

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 (Aug 15 2020 at 05:33):

@Adam Topaz

Aaron Anderson (Aug 15 2020 at 06:28):

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

Aaron Anderson (Aug 15 2020 at 06:28):

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

Adam Topaz (Aug 15 2020 at 14:34):

@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 (Aug 15 2020 at 14:37):

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 (Aug 15 2020 at 14:46):

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

Johan Commelin (Aug 15 2020 at 14:46):

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

Adam Topaz (Aug 15 2020 at 16:48):

@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 (Aug 15 2020 at 17:34):

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

Aaron Anderson (Aug 15 2020 at 17:52):

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 (Aug 15 2020 at 17:54):

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

Adam Topaz (Aug 15 2020 at 17:55):

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

Jack J Garzella (Aug 16 2020 at 01:07):

@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 (Aug 16 2020 at 01:08):

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 (Aug 16 2020 at 02:10):

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 (Aug 18 2020 at 01:02):

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


Last updated: Dec 20 2023 at 11:08 UTC