# Documentation

Mathlib.FieldTheory.Perfect

# Perfect fields and rings #

In this file we define perfect fields, together with a generalisation to (commutative) rings in prime characteristic.

## Main definitions / statements: #

• PerfectRing: a ring of characteristic p (prime) is said to be perfect in the sense of Serre, if its absolute Frobenius map x ↦ xᵖ is bijective.
• PerfectField: a field K is said to be perfect if every irreducible polynomial over K is separable.
• PerfectRing.toPerfectField: a field that is perfect in the sense of Serre is a perfect field.
• PerfectField.toPerfectRing: a perfect field of characteristic p (prime) is perfect in the sense of Serre.
• PerfectField.ofCharZero: all fields of characteristic zero are perfect.
• PerfectField.ofFinite: all finite fields are perfect.
class PerfectRing (R : Type u_1) (p : ) [] [Fact ()] [CharP R p] :
• bijective_frobenius : Function.Bijective ↑()

A ring is perfect if the Frobenius map is bijective.

A perfect ring of characteristic p (prime) in the sense of Serre.

NB: This is not related to the concept with the same name introduced by Bass (related to projective covers of modules).

Instances
theorem PerfectRing.ofSurjective (R : Type u_1) (p : ) [] [Fact ()] [CharP R p] [] (h : Function.Surjective ↑()) :

For a reduced ring, surjectivity of the Frobenius map is a sufficient condition for perfection.

instance PerfectRing.ofFiniteOfIsReduced (p : ) [Fact ()] (R : Type u_1) [] [CharP R p] [] [] :
@[simp]
theorem bijective_frobenius (R : Type u_1) (p : ) [] [Fact ()] [CharP R p] [] :
@[simp]
theorem injective_frobenius (R : Type u_1) (p : ) [] [Fact ()] [CharP R p] [] :
@[simp]
theorem surjective_frobenius (R : Type u_1) (p : ) [] [Fact ()] [CharP R p] [] :
@[simp]
theorem frobeniusEquiv_apply (R : Type u_1) (p : ) [] [Fact ()] [CharP R p] [] (a : R) :
↑() a = ↑() a
noncomputable def frobeniusEquiv (R : Type u_1) (p : ) [] [Fact ()] [CharP R p] [] :
R ≃+* R

The Frobenius automorphism for a perfect ring.

Instances For
@[simp]
theorem coe_frobeniusEquiv (R : Type u_1) (p : ) [] [Fact ()] [CharP R p] [] :
↑() = ↑()
@[simp]
theorem frobeniusEquiv_symm_apply_frobenius (R : Type u_1) (p : ) [] [Fact ()] [CharP R p] [] (x : R) :
↑() (↑() x) = x
@[simp]
theorem frobenius_apply_frobeniusEquiv_symm (R : Type u_1) (p : ) [] [Fact ()] [CharP R p] [] (x : R) :
↑() (↑() x) = x
@[simp]
theorem frobenius_comp_frobeniusEquiv_symm (R : Type u_1) (p : ) [] [Fact ()] [CharP R p] [] :
RingHom.comp () ↑() =
@[simp]
theorem frobeniusEquiv_symm_comp_frobenius (R : Type u_1) (p : ) [] [Fact ()] [CharP R p] [] :
RingHom.comp (↑()) () =
@[simp]
theorem frobeniusEquiv_symm_pow_p (R : Type u_1) (p : ) [] [Fact ()] [CharP R p] [] (x : R) :
↑() x ^ p = x
theorem injective_pow_p (R : Type u_1) (p : ) [] [Fact ()] [CharP R p] [] {x : R} {y : R} (h : x ^ p = y ^ p) :
x = y
theorem polynomial_expand_eq (R : Type u_1) (p : ) [] [Fact ()] [CharP R p] [] (f : ) :
↑() f = Polynomial.map (↑()) f ^ p
@[simp]
theorem not_irreducible_expand (R : Type u_1) (p : ) [] [Fact ()] [CharP R p] [] (f : ) :
¬Irreducible (↑() f)
class PerfectField (K : Type u_1) [] :
• separable_of_irreducible : ∀ {f : },

A field is perfect if every irreducible polynomial is separable.

A perfect field.

See also PerfectRing for a generalisation in positive characteristic.

Instances
theorem PerfectRing.toPerfectField (K : Type u_1) (p : ) [] [hp : Fact ()] [CharP K p] [] :
instance PerfectField.ofCharZero (K : Type u_1) [] [] :
instance PerfectField.ofFinite (K : Type u_1) [] [] :
instance PerfectField.toPerfectRing (K : Type u_1) [] [] (p : ) [hp : Fact ()] [CharP K p] :

A perfect field of characteristic p (prime) is a perfect ring.