# 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.
• PerfectField.separable_iff_squarefree: a polynomial over a perfect field is separable iff it is square-free.
• Algebra.IsAlgebraic.isSeparable_of_perfectField, Algebra.IsAlgebraic.perfectField: if L / K is an algebraic extension, K is a perfect field, then L / K is separable, and L is also a perfect field.
class PerfectRing (R : Type u_1) (p : ) [] [ExpChar R p] :

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.bijective_frobenius {R : Type u_1} {p : } [] [ExpChar R p] [self : ] :

A ring is perfect if the Frobenius map is bijective.

theorem PerfectRing.ofSurjective (R : Type u_2) (p : ) [] [ExpChar R p] [] (h : Function.Surjective (frobenius R p)) :

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

instance PerfectRing.ofFiniteOfIsReduced (p : ) (R : Type u_2) [] [ExpChar R p] [] [] :
Equations
• =
@[simp]
theorem bijective_frobenius (R : Type u_1) (p : ) [] [ExpChar R p] [] :
theorem bijective_iterateFrobenius (R : Type u_1) (p : ) (n : ) [] [ExpChar R p] [] :
@[simp]
theorem injective_frobenius (R : Type u_1) (p : ) [] [ExpChar R p] [] :
@[simp]
theorem surjective_frobenius (R : Type u_1) (p : ) [] [ExpChar R p] [] :
@[simp]
theorem frobeniusEquiv_apply (R : Type u_1) (p : ) [] [ExpChar R p] [] (a : R) :
(frobeniusEquiv R p) a = (frobenius R p) a
noncomputable def frobeniusEquiv (R : Type u_1) (p : ) [] [ExpChar R p] [] :
R ≃+* R

The Frobenius automorphism for a perfect ring.

Equations
Instances For
@[simp]
theorem coe_frobeniusEquiv (R : Type u_1) (p : ) [] [ExpChar R p] [] :
(frobeniusEquiv R p) = (frobenius R p)
theorem frobeniusEquiv_def (R : Type u_1) (p : ) [] [ExpChar R p] [] (x : R) :
(frobeniusEquiv R p) x = x ^ p
@[simp]
theorem iterateFrobeniusEquiv_apply (R : Type u_1) (p : ) (n : ) [] [ExpChar R p] [] (a : R) :
a = (iterateFrobenius R p n) a
noncomputable def iterateFrobeniusEquiv (R : Type u_1) (p : ) (n : ) [] [ExpChar R p] [] :
R ≃+* R

The iterated Frobenius automorphism for a perfect ring.

Equations
Instances For
@[simp]
theorem coe_iterateFrobeniusEquiv (R : Type u_1) (p : ) (n : ) [] [ExpChar R p] [] :
= (iterateFrobenius R p n)
theorem iterateFrobeniusEquiv_def (R : Type u_1) (p : ) (n : ) [] [ExpChar R p] [] (x : R) :
x = x ^ p ^ n
theorem iterateFrobeniusEquiv_add_apply (R : Type u_1) (p : ) (m : ) (n : ) [] [ExpChar R p] [] (x : R) :
(iterateFrobeniusEquiv R p (m + n)) x = ( x)
theorem iterateFrobeniusEquiv_add (R : Type u_1) (p : ) (m : ) (n : ) [] [ExpChar R p] [] :
iterateFrobeniusEquiv R p (m + n) = .trans
theorem iterateFrobeniusEquiv_symm_add_apply (R : Type u_1) (p : ) (m : ) (n : ) [] [ExpChar R p] [] (x : R) :
(iterateFrobeniusEquiv R p (m + n)).symm x = .symm (.symm x)
theorem iterateFrobeniusEquiv_symm_add (R : Type u_1) (p : ) (m : ) (n : ) [] [ExpChar R p] [] :
(iterateFrobeniusEquiv R p (m + n)).symm = .symm.trans .symm
theorem iterateFrobeniusEquiv_zero_apply (R : Type u_1) (p : ) [] [ExpChar R p] [] (x : R) :
x = x
theorem iterateFrobeniusEquiv_one_apply (R : Type u_1) (p : ) [] [ExpChar R p] [] (x : R) :
x = x ^ p
@[simp]
theorem iterateFrobeniusEquiv_zero (R : Type u_1) (p : ) [] [ExpChar R p] [] :
@[simp]
theorem iterateFrobeniusEquiv_one (R : Type u_1) (p : ) [] [ExpChar R p] [] :
=
theorem iterateFrobeniusEquiv_eq_pow (R : Type u_1) (p : ) (n : ) [] [ExpChar R p] [] :
= ^ n
theorem iterateFrobeniusEquiv_symm (R : Type u_1) (p : ) (n : ) [] [ExpChar R p] [] :
.symm = (frobeniusEquiv R p).symm ^ n
@[simp]
theorem frobeniusEquiv_symm_apply_frobenius (R : Type u_1) (p : ) [] [ExpChar R p] [] (x : R) :
(frobeniusEquiv R p).symm ((frobenius R p) x) = x
@[simp]
theorem frobenius_apply_frobeniusEquiv_symm (R : Type u_1) (p : ) [] [ExpChar R p] [] (x : R) :
(frobenius R p) ((frobeniusEquiv R p).symm x) = x
@[simp]
theorem frobenius_comp_frobeniusEquiv_symm (R : Type u_1) (p : ) [] [ExpChar R p] [] :
(frobenius R p).comp (frobeniusEquiv R p).symm =
@[simp]
theorem frobeniusEquiv_symm_comp_frobenius (R : Type u_1) (p : ) [] [ExpChar R p] [] :
(↑(frobeniusEquiv R p).symm).comp (frobenius R p) =
@[simp]
theorem frobeniusEquiv_symm_pow_p (R : Type u_1) (p : ) [] [ExpChar R p] [] (x : R) :
(frobeniusEquiv R p).symm x ^ p = x
theorem injective_pow_p (R : Type u_1) (p : ) [] [ExpChar R p] [] {x : R} {y : R} (h : x ^ p = y ^ p) :
x = y
theorem polynomial_expand_eq (R : Type u_1) (p : ) [] [ExpChar R p] [] (f : ) :
f = Polynomial.map (↑(frobeniusEquiv R p).symm) f ^ p
@[simp]
theorem not_irreducible_expand (R : Type u_2) (p : ) [] [Fact (Nat.Prime p)] [CharP R p] [] (f : ) :
instance instPerfectRingProd (R : Type u_1) (p : ) [] [ExpChar R p] [] (S : Type u_2) [] [ExpChar S p] [] :
PerfectRing (R × S) p
Equations
• =
class PerfectField (K : Type u_1) [] :

A perfect field.

See also PerfectRing for a generalisation in positive characteristic.

• separable_of_irreducible : ∀ {f : }, f.Separable

A field is perfect if every irreducible polynomial is separable.

Instances
theorem PerfectField.separable_of_irreducible {K : Type u_1} [] [self : ] {f : } :
f.Separable

A field is perfect if every irreducible polynomial is separable.

theorem PerfectRing.toPerfectField (K : Type u_1) (p : ) [] [ExpChar K p] [] :
instance PerfectField.ofCharZero {K : Type u_1} [] [] :
Equations
• =
instance PerfectField.ofFinite {K : Type u_1} [] [] :
Equations
• =
instance PerfectField.toPerfectRing {K : Type u_1} [] [] (p : ) [ExpChar K p] :

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

Equations
• =
theorem PerfectField.separable_iff_squarefree {K : Type u_1} [] [] {g : } :
g.Separable
instance Algebra.IsAlgebraic.isSeparable_of_perfectField {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] [] [] :

If L / K is an algebraic extension, K is a perfect field, then L / K is separable.

Equations
• =
theorem Algebra.IsAlgebraic.perfectField {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] [] [] :

If L / K is an algebraic extension, K is a perfect field, then so is L.

theorem Polynomial.roots_expand_pow_map_iterateFrobenius_le {R : Type u_1} [] [] (p : ) (n : ) [ExpChar R p] (f : ) :
Multiset.map (⇑(iterateFrobenius R p n)) ((Polynomial.expand R (p ^ n)) f).roots p ^ n f.roots
theorem Polynomial.roots_expand_map_frobenius_le {R : Type u_1} [] [] (p : ) [ExpChar R p] (f : ) :
Multiset.map (⇑(frobenius R p)) ( f).roots p f.roots
theorem Polynomial.roots_expand_pow_image_iterateFrobenius_subset {R : Type u_1} [] [] (p : ) (n : ) [ExpChar R p] (f : ) [] :
Finset.image (⇑(iterateFrobenius R p n)) ((Polynomial.expand R (p ^ n)) f).roots.toFinset f.roots.toFinset
theorem Polynomial.roots_expand_image_frobenius_subset {R : Type u_1} [] [] (p : ) [ExpChar R p] (f : ) [] :
Finset.image (⇑(frobenius R p)) ( f).roots.toFinset f.roots.toFinset
theorem Polynomial.roots_expand_pow {R : Type u_1} [] [] {p : } {n : } [ExpChar R p] {f : } [] :
((Polynomial.expand R (p ^ n)) f).roots = p ^ n Multiset.map (⇑.symm) f.roots
theorem Polynomial.roots_expand {R : Type u_1} [] [] {p : } [ExpChar R p] {f : } [] :
( f).roots = p Multiset.map (⇑(frobeniusEquiv R p).symm) f.roots
theorem Polynomial.roots_X_pow_char_pow_sub_C {R : Type u_1} [] [] {p : } {n : } [ExpChar R p] [] {y : R} :
(Polynomial.X ^ p ^ n - Polynomial.C y).roots = p ^ n {.symm y}
theorem Polynomial.roots_X_pow_char_pow_sub_C_pow {R : Type u_1} [] [] {p : } {n : } [ExpChar R p] [] {y : R} {m : } :
((Polynomial.X ^ p ^ n - Polynomial.C y) ^ m).roots = (m * p ^ n) {.symm y}
theorem Polynomial.roots_X_pow_char_sub_C {R : Type u_1} [] [] {p : } [ExpChar R p] [] {y : R} :
(Polynomial.X ^ p - Polynomial.C y).roots = p {(frobeniusEquiv R p).symm y}
theorem Polynomial.roots_X_pow_char_sub_C_pow {R : Type u_1} [] [] {p : } [ExpChar R p] [] {y : R} {m : } :
((Polynomial.X ^ p - Polynomial.C y) ^ m).roots = (m * p) {(frobeniusEquiv R p).symm y}
theorem Polynomial.roots_expand_pow_map_iterateFrobenius {R : Type u_1} [] [] {p : } {n : } [ExpChar R p] {f : } [] :
Multiset.map (⇑(iterateFrobenius R p n)) ((Polynomial.expand R (p ^ n)) f).roots = p ^ n f.roots
theorem Polynomial.roots_expand_map_frobenius {R : Type u_1} [] [] {p : } [ExpChar R p] {f : } [] :
Multiset.map (⇑(frobenius R p)) ( f).roots = p f.roots
theorem Polynomial.roots_expand_image_iterateFrobenius {R : Type u_1} [] [] {p : } {n : } [ExpChar R p] {f : } [] [] :
Finset.image (⇑(iterateFrobenius R p n)) ((Polynomial.expand R (p ^ n)) f).roots.toFinset = f.roots.toFinset
theorem Polynomial.roots_expand_image_frobenius {R : Type u_1} [] [] {p : } [ExpChar R p] {f : } [] [] :
Finset.image (⇑(frobenius R p)) ( f).roots.toFinset = f.roots.toFinset
noncomputable def Polynomial.rootsExpandToRoots {R : Type u_1} [] [] (p : ) [ExpChar R p] (f : ) [] :
{ x : R // x ( f).roots.toFinset } { x : R // x f.roots.toFinset }

If f is a polynomial over an integral domain R of characteristic p, then there is a map from the set of roots of Polynomial.expand R p f to the set of roots of f. It's given by x ↦ x ^ p, see rootsExpandToRoots_apply.

Equations
• = { toFun := fun (x : { x : R // x ( f).roots.toFinset }) => x ^ p, , inj' := }
Instances For
@[simp]
theorem Polynomial.rootsExpandToRoots_apply {R : Type u_1} [] [] (p : ) [ExpChar R p] (f : ) [] (x : { x : R // x ( f).roots.toFinset }) :
( x) = x ^ p
noncomputable def Polynomial.rootsExpandPowToRoots {R : Type u_1} [] [] (p : ) (n : ) [ExpChar R p] (f : ) [] :
{ x : R // x ((Polynomial.expand R (p ^ n)) f).roots.toFinset } { x : R // x f.roots.toFinset }

If f is a polynomial over an integral domain R of characteristic p, then there is a map from the set of roots of Polynomial.expand R (p ^ n) f to the set of roots of f. It's given by x ↦ x ^ (p ^ n), see rootsExpandPowToRoots_apply.

Equations
• = { toFun := fun (x : { x : R // x ((Polynomial.expand R (p ^ n)) f).roots.toFinset }) => x ^ p ^ n, , inj' := }
Instances For
@[simp]
theorem Polynomial.rootsExpandPowToRoots_apply {R : Type u_1} [] [] (p : ) (n : ) [ExpChar R p] (f : ) [] (x : { x : R // x ((Polynomial.expand R (p ^ n)) f).roots.toFinset }) :
( x) = x ^ p ^ n
noncomputable def Polynomial.rootsExpandEquivRoots {R : Type u_1} [] [] (p : ) [ExpChar R p] (f : ) [] [] :
{ x : R // x ( f).roots.toFinset } { x : R // x f.roots.toFinset }

If f is a polynomial over a perfect integral domain R of characteristic p, then there is a bijection from the set of roots of Polynomial.expand R p f to the set of roots of f. It's given by x ↦ x ^ p, see rootsExpandEquivRoots_apply.

Equations
Instances For
@[simp]
theorem Polynomial.rootsExpandEquivRoots_apply {R : Type u_1} [] [] (p : ) [ExpChar R p] (f : ) [] [] (x : { x : R // x ( f).roots.toFinset }) :
( x) = x ^ p
noncomputable def Polynomial.rootsExpandPowEquivRoots {R : Type u_1} [] [] (p : ) [ExpChar R p] (f : ) [] [] (n : ) :
{ x : R // x ((Polynomial.expand R (p ^ n)) f).roots.toFinset } { x : R // x f.roots.toFinset }

If f is a polynomial over a perfect integral domain R of characteristic p, then there is a bijection from the set of roots of Polynomial.expand R (p ^ n) f to the set of roots of f. It's given by x ↦ x ^ (p ^ n), see rootsExpandPowEquivRoots_apply.

Equations
Instances For
@[simp]
theorem Polynomial.rootsExpandPowEquivRoots_apply {R : Type u_1} [] [] (p : ) [ExpChar R p] (f : ) [] [] (n : ) (x : { x : R // x ((Polynomial.expand R (p ^ n)) f).roots.toFinset }) :
( x) = x ^ p ^ n