Zulip Chat Archive

Stream: maths

Topic: Galois theory


view this post on Zulip Johan Commelin (Nov 27 2020 at 07:55):

Major kudos to @Thomas Browning @Patrick Lutz and others from the Berkeley clan. Galois theory for finite extensions will come to mathlib as soon as bors is happy!
Fantastic work! Galois correspondences ftw.
:tada: :octopus: :clink: :smiley: :top_hat: :cake: :dancing:

view this post on Zulip Kenny Lau (Nov 27 2020 at 08:01):

what's the galois emote

view this post on Zulip Adam Topaz (Nov 27 2020 at 14:18):

π1eˊt\pi_1^\text{\'et} by 2022?

view this post on Zulip Ruben Van de Velde (Nov 27 2020 at 15:34):

Surely not :swords: , he was shot

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 15:34):

d'oh

view this post on Zulip Johan Commelin (Nov 27 2020 at 15:36):

/me :gun: :gun: (oh, the joys of postmodern emoji's)

view this post on Zulip Johan Commelin (Nov 27 2020 at 17:16):

Adam Topaz said:

π1eˊt\pi_1^\text{\'et} by 2022?

We have the category of schemes, we have Grothendieck topologies... we really need to get etale ring homs.

view this post on Zulip Adam Topaz (Nov 27 2020 at 17:30):

I think galois categories would be a nice project all by itself.

view this post on Zulip Adam Topaz (Nov 27 2020 at 17:31):

But I've been wondering about the best way to go about this. Maybe it makes sense to prove Barr-Beck first?

view this post on Zulip Adam Topaz (Nov 27 2020 at 17:33):

@Johan Commelin you forgot that we also now have algebraically closed fields (you need base points!)

view this post on Zulip Johan Commelin (Nov 27 2020 at 17:35):

Sure, good point.

view this post on Zulip Adam Topaz (Nov 27 2020 at 17:38):

Do we have non-algebraic separable extensions? (of fields)

view this post on Zulip Johan Commelin (Nov 27 2020 at 17:41):

Nope, I think in mathlib separable extensions are algebraic by assumption.

view this post on Zulip Thomas Browning (Nov 27 2020 at 17:45):

That's right. An extension is separable if every element is integral and its minimal polynomial is separable (or something like that)

view this post on Zulip Adam Topaz (Nov 27 2020 at 17:50):

@Thomas Browning There is a perfectly good notion of separability for nonalgebraic extensions. I was asking what the situation was in mathlib.

view this post on Zulip Thomas Browning (Nov 27 2020 at 17:51):

Sorry, to clarify: I think that what I gave is the mathlib definition

view this post on Zulip Johan Commelin (Nov 27 2020 at 17:53):

https://en.wikipedia.org/wiki/Separable_extension#Separability_of_transcendental_extensions

Sounds like we can almost write down the statement of the TFAE mentioned there


Last updated: May 06 2021 at 18:20 UTC