Topic: Galois theory
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:
Kenny Lau (Nov 27 2020 at 08:01):
what's the galois emote
Adam Topaz (Nov 27 2020 at 14:18):
Ruben Van de Velde (Nov 27 2020 at 15:34):
Surely not :swords: , he was shot
Kevin Buzzard (Nov 27 2020 at 15:34):
Johan Commelin (Nov 27 2020 at 15:36):
:gun: :gun: (oh, the joys of postmodern emoji's)
Johan Commelin (Nov 27 2020 at 17:16):
Adam Topaz said:
We have the category of schemes, we have Grothendieck topologies... we really need to get etale ring homs.
Adam Topaz (Nov 27 2020 at 17:30):
I think galois categories would be a nice project all by itself.
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?
Adam Topaz (Nov 27 2020 at 17:33):
@Johan Commelin you forgot that we also now have algebraically closed fields (you need base points!)
Johan Commelin (Nov 27 2020 at 17:35):
Sure, good point.
Adam Topaz (Nov 27 2020 at 17:38):
Do we have non-algebraic separable extensions? (of fields)
Johan Commelin (Nov 27 2020 at 17:41):
Nope, I think in mathlib separable extensions are algebraic by assumption.
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)
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.
Thomas Browning (Nov 27 2020 at 17:51):
Sorry, to clarify: I think that what I gave is the mathlib definition
Johan Commelin (Nov 27 2020 at 17:53):
Sounds like we can almost write down the statement of the TFAE mentioned there
Last updated: May 06 2021 at 18:20 UTC