Perfect Fields

This entry provides a type class for perfect fields. A perfect field K can be characterized by one of the following equivalent conditions:

• Any irreducible polynomial p is separable, i.e. gcd(p,p') = 1, or, equivalently, p' non-zero.
• Either the characteristic of K is 0 or p > 0 and the Frobenius endomorphism is surjective (i.e. every element of K has a p-th root).

We define perfect fields using the second characterization and show the equivalence to the first characterization. The implication ``2 => 1'' is relatively straightforward using the injectivity of the Frobenius homomorphism. Examples for perfect fields are:

• any field of characteristic 0 (e.g. the reals or complex numbers)
• any finite field (i.e. F_q for q=pⁿ, n > 0 and p prime)
• any algebraically closed field (for example the formal Puiseux series over finite fields)