Zulip Chat Archive

Stream: maths

Topic: Real Closed Fields


view this post on Zulip Aaron Anderson (Aug 15 2020 at 05:31):

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

view this post on Zulip 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.

view this post on Zulip Aaron Anderson (Aug 15 2020 at 05:33):

@Adam Topaz

view this post on Zulip Aaron Anderson (Aug 15 2020 at 06:28):

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

view this post on Zulip Aaron Anderson (Aug 15 2020 at 06:28):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Aug 15 2020 at 14:46):

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

view this post on Zulip Johan Commelin (Aug 15 2020 at 14:46):

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

view this post on Zulip 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).

view this post on Zulip Johan Commelin (Aug 15 2020 at 17:34):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Aug 15 2020 at 17:54):

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

view this post on Zulip Adam Topaz (Aug 15 2020 at 17:55):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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: May 10 2021 at 07:15 UTC