### Abstract

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. Fq for q=pn, n > 0 and p prime)
- any algebraically closed field (for example the formal Puiseux series over finite fields)

### License

BSD License

### Topics

- Mathematics/Algebra

### Session Perfect_Fields

- Perfect_Field_Library
- Perfect_Fields
- Perfect_Field_Algebraically_Closed
- Algebraic_Closure_Type
- Perfect_Field_Altdef

### Depends on

- The Factorization Algorithm of Berlekamp and Zassenhaus
- Formal Puiseux Series

### Used by

- Elimination of Repeated Factors Algorithm

### Auto-related entries

- Finite Fields
- Universal Hash Families
- Hilbert’s Nullstellensatz
- Lehmer’s Theorem

## Cite

×

Perfect_Fields-AFP

    @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},
    }

Download

## Download

× Download latest