Solvable field extensions

Stream: Berkeley Lean Seminar

[Patrick Lutz]

Would it be helpful to explicitly define (and provide notation for?) the automorphism group $Aut(E/F)$, the notion of a field extension being solvable (galois and automorphism group is solvable? Or maybe just automorphism group is solvable?) and the notion of an algebraic element being solvable (splitting field is solvable)? It's kind of annoying to have to write things like

  is_solvable ((minimal_polynomial (is_integral α)).splitting_field ≃ₐ[F]
    (minimal_polynomial (is_integral α)).splitting_field)

[Thomas Browning]

Notation would be good. Right now I'm using P for that prop you wrote out.

[Kevin Buzzard]

I like the idea of a predicate is_solvable on elements of a field extension; this seems like a natural predicate because it's closed under + - * / .

[Thomas Browning]

should we have two predicates: is_SBR and is_solvable that turn out to be the same?

[Kevin Buzzard]

No

[Kevin Buzzard]

Each definition comes with pain.

[Kevin Buzzard]

A definition is either useless or has a bunch of theorems proved about it to make it useful. So you want as few as possible, because it's hard work to make a definition useful!

[Thomas Browning]

Currently we have a predicate is_SBR that automatically defines an intermediate_field

[Kevin Buzzard]

What's it a predicate on?

[Kevin Buzzard]

If it's on elements then it sounds like you have this predicate already.

[Thomas Browning]

elements of E (if E is an arbitrary extension of F)

[Kevin Buzzard]

So "the notion of an algebraic element being solvable" which you mentioned above -- sounds like you have this.

[Thomas Browning]

that predicate is just inductively constructed from the field operations and taking roots

[Thomas Browning]

rather than being: minimal polynomial has solvable galois group

[Kevin Buzzard]

So that's the theorem you want to prove.

[Thomas Browning]

yes, the problem is that it's annoying to write "minimal polynomial has solvable galois group"

[Kevin Buzzard]

Aah I see! But you don't have to write it once you've proved the theorem :-)

[Thomas Browning]

true, but when proving the theorem you don't want to have to keep writing

  is_solvable ((minimal_polynomial (is_integral α)).splitting_field ≃ₐ[F]
    (minimal_polynomial (is_integral α)).splitting_field)

[Kevin Buzzard]

Definitely don't make a second definition which turns out to be equivalent to something you have already. If you do this then you'll find that you'll have to choose which one of them is the "normal form" for e.g. simp lemmas, and then you'll realise that the other one is useless.

[Kevin Buzzard]

I would definitely be tempted to make notation for Gal(E/F), looking at what you have there.

[Kevin Buzzard]

but don't make new definitions if you can possibly help it.

[Thomas Browning]

you mean, make notation for Galois group of an element?

[Kevin Buzzard]

is_solvable (Gal (splitting_field alpha) F) -- would that be OK?

[Kevin Buzzard]

spl alpha?

[Kevin Buzzard]

Or maybe F (splitting_field alpha) -- is that the way it usually is?

[Thomas Browning]

Kevin Buzzard said:

is_solvable (Gal (splitting_field alpha) F) -- would that be OK?

seems reasonable

[Kevin Buzzard]

Gal(E/F) is one of those weird things where the Lean people would say "just define it for an arbitrary F-algebra E" and the maths people go "aargh no"

[Kevin Buzzard]

I think I'd be tempted to call it Aut F E

[Kevin Buzzard]

hmm except that it's then not clear that it's F-algebra auts I guess, it could be F-module auts.