Galois theory

Stream: maths

[Johan Commelin]

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]

what's the galois emote

[Adam Topaz]

$\pi_1^\text{\'et}$ by 2022?

[Ruben Van de Velde]

Surely not :swords: , he was shot

[Kevin Buzzard]

d'oh

[Johan Commelin]

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

[Johan Commelin]

Adam Topaz said:

$\pi_1^\text{\'et}$ by 2022?

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Johan Commelin]

Sure, good point.

[Adam Topaz]

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

[Johan Commelin]

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

[Thomas Browning]

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

[Adam Topaz]

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

[Thomas Browning]

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

[Johan Commelin]

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