## Stream: maths

### 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.

#### Kenny Lau (Nov 27 2020 at 08:01):

what's the galois emote

#### Adam Topaz (Nov 27 2020 at 14:18):

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

#### Ruben Van de Velde (Nov 27 2020 at 15:34):

Surely not :swords: , he was shot

d'oh

#### Johan Commelin (Nov 27 2020 at 15:36):

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

#### Johan Commelin (Nov 27 2020 at 17:16):

$\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 (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: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):

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