Roadmap to algebraic closure of field F

Implicitly, in what I write below, p=1 if char(F)=0.

Field theory

Any finite subgroup of F* is cyclic
Freshman's dream: (x+y)^p = x^p + y^p

Polynomials

division algorithm
F[X] is a ED (3)
ED -> PID -> UFD -> GCD
F[X] is a PID (4,5)
F[X] is a UFD (4,5)
F[X] is a GCD (4,5)

Algebraic extensions

Integral elements form subring

Splitting fields

Every polynomial splits in some extension (6,7)

Separable polynomials

Resultant of two polynomials
Discriminant of polynomials (11)
f in F[X] is separable := discriminant(f) is non-zero (12)
f is separable iff gcd(f,Df)=1 (8,11)
f is separable iff it has no double root in every extension in which it splits (10)
For every irreducible f in F[X] there is n in N and h in F[X] such that f(x) = h(x^(p^n)) and h is separable (14)
If If K/F then f in F[X] is separable iff (coe f) in K[X] is separable. (13)
f is separable iff all its factors are separable
Primitive element theorem (1,10,15,17,18)
F perfect := every polynomial is separable
Perfect iff Frobenius surjective (2,16)

Proof

For every irreducible f in F[X] let Xf be an indeterminate.
Let R := F[{Xf | f irredcuible}] be a big polynomial ring.
Let I := span {f(Xf) | f irreducible} an ideal in R.
I is a proper ideal. (10)
Let L := R/M where M is a maximal ideal that contains I (25).
L is a field algebraic over F. (9)
Let K := {x in L | exists n, x^(p^n) in F}.
K is a subfield. (2)
K is perfect. (2,21)
Every polynomial in K[X] has a root in L. (2)
Every polynomial in K[X] splits in L. (19,30,31)
L is algebraically closed. (32)
L is an algebraic closure of F. (27,33)