Abstract

This entry provides a type class for perfect fields. A perfect field K can be characterized by one of the following equivalent conditions:
1. Any irreducible polynomial p is separable, i.e. gcd(p,p’) = 1, or, equivalently, p’ is non-zero.
2. 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 in one direction is relatively straightforward using the injectivity of the Frobenius homomorphism. Examples for perfect fields are:
1. any field of characteristic 0 (e.g. the reals or complex numbers), 2. any finite field, 3. any algebraically closed field.

BibTeX

@article{Perfect_Fields-AFP,
  author  = {Manuel Eberl and Katharina Kreuzer},
  title   = {Perfect Fields},
  journal = {Archive of Formal Proofs},
  month   = {November},
  year    = {2023},
  note    = {\url{https://isa-afp.org/entries/Perfect_Fields.html},
             Formal proof development},
  ISSN    = {2150-914x},
}