Abel-Ruffini theorem

[pglutz]

Here is a list of things to do in order to prove the Abel-Ruffini theorem. In all the steps below, I will assume that E is a field extension of a field F and primarily talk about intermediate_fields of E/F.

Check things off as you do them and maybe edit the list to link to the line number of the relevant theorem on github (or not, if that's too annoying)

Facts about fields

• If L < K are intermediate_fields of E/F then K is an L algebra
• If K_1 < K_2 < K_3 are intermediate_fields of E/F then they form an is_scalar_tower
• If L < K are intermediate_fields of E/F which are both galois over F then the galois group of K/F surjects onto the galois group of L/F (or maybe just assume F, L, K form an is_scalar_tower?)
• If L contains the nth roots of unity and K/L is obtained by adjoining an nth root of something in L then K/L is galois with abelian (cyclic) galois group. In fact, its galois group injects into Z/nZ
• If L and K are intermediate_fields which are both galois over F then the compositum (sup K L) is also galois over F and the galois group embeds into the product of the galois groups of K/F and L/F.
• If a = b + c and everything algebraic over F then the splitting field of the minimal polynomial of a is contained in the compositum of the splitting fields of the minimal polynomials of b and c.
• If F, L, E form an is_scalar_tower (nothing here is an intermediate_field) and L/F, E/L and E/F are all galois then their galois groups form a short exact sequence
• There is an irreducible polynomial p such that the splitting field of p has galois group isomorphic to S_5 (for whatever version of S_5 is proved not solvable below)
• If p is an irreducible polynomial then the minimal polynomial of any root of p is p itself

Facts about groups

• Product of solvable groups is solvable
• If a solvable group surjects onto a group then that group is also solvable link
• Abelian groups are solvable
• If a group is the middle term in a short exact sequence of solvable groups then it is solvable.
• S_5 is not solvable (really, just prove the group of permutations on some 5 element type is not solvable)

Facts about solvability of galois groups

• If F, L, E form an is_scalar_tower (nothing here is an intermediate_field) such that L/F and E/L are both galois and solvable and E/F is galois then E/F is solvable.
• If L contains the nth roots of unity and K/L is obtained by adjoining an nth root of something in L then K/L is galois with solvable galois group
• If L < K and everything galois and K/F is solvable then L/F is solvable

Abel-Ruffini theorem

• Define solvable_by_radicals a for a in E. This is just a prop-valued inductive type, as described in this thread.
• Show by induction that if solvable_by_radicals a then a is algebraic (or is_integral) over F
  • Base case and cases +, *, - have already been done
  • Case ^-1 should be easy
  • Case ^(1/n) should be easy (p(X^n))
• Show by induction that if solvable_by_radicals a then the splitting field of the minimal polynomial of a over F is solvable
  • Base case is easy
  • Case ^-1 should be easy
  • Cases +, *, - correspond to compositum.
  • Case a^n = b can be done as follows: form a sequence of intermediate_fields, F = K_0 < K_1 < K_2 < ... < K_m where K_1 is the splitting field of p (min. poly. of b), K_2 is obtained by adjoining the nth roots of unity and each extension after is obtained by adjoining nth root of a root of p. Next, show that K_m is equal to the splitting field of p(X^n)(X^n - 1), hence galois. Finally, show by backwards induction on i that K_m is solvable over K_i. Finally, observe that the min. poly. of a divides p(X^n)(X^n - 1), hence its splitting field is contained in K_m, hence its galois group embeds into K_m's and hence is solvable
• Let p be the polynomial whose galois group is S_5. If solvable_by_radicals a holds for any root of p then the splitting field of the minimal polynomial of that root is solvable. But the minimal polynomial of such a root must be p itself so S_5 is solvable. Contradiction.