# 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.

source
class PerfectRing (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] :
Prop

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).

- bijective_frobenius : Function.Bijective ⇑(frobenius R p)

  A ring is perfect if the Frobenius map is bijective.

Instances

source
theorem PerfectRing.ofSurjective (R : Type u_2) (p : ℕ) [CommRing R] [ExpChar R p] [IsReduced R] (h : Function.Surjective ⇑(frobenius R p)) :
PerfectRing R p

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

source
instance PerfectRing.ofFiniteOfIsReduced (p : ℕ) (R : Type u_2) [CommRing R] [ExpChar R p] [Finite R] [IsReduced R] :
PerfectRing R p
source
@[simp]
theorem bijective_frobenius (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
Function.Bijective ⇑(frobenius R p)
source
theorem bijective_iterateFrobenius (R : Type u_1) (p n : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
Function.Bijective ⇑(iterateFrobenius R p n)
source
@[simp]
theorem injective_frobenius (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
Function.Injective ⇑(frobenius R p)
source
@[simp]
theorem surjective_frobenius (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
Function.Surjective ⇑(frobenius R p)
source
noncomputable def frobeniusEquiv (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
R ≃+* R

The Frobenius automorphism for a perfect ring.

Equations

- frobeniusEquiv R p = RingEquiv.ofBijective (frobenius R p) ⋯

Instances For

source
@[simp]
theorem frobeniusEquiv_apply (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (a : R) :
(frobeniusEquiv R p) a = (frobenius R p) a
source
@[simp]
theorem coe_frobeniusEquiv (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
⇑(frobeniusEquiv R p) = ⇑(frobenius R p)
source
theorem frobeniusEquiv_def (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) :
(frobeniusEquiv R p) x = x ^ p
source
noncomputable def iterateFrobeniusEquiv (R : Type u_1) (p n : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
R ≃+* R

The iterated Frobenius automorphism for a perfect ring.

Equations

- iterateFrobeniusEquiv R p n = RingEquiv.ofBijective (iterateFrobenius R p n) ⋯

Instances For

source
@[simp]
theorem iterateFrobeniusEquiv_apply (R : Type u_1) (p n : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (a : R) :
(iterateFrobeniusEquiv R p n) a = (iterateFrobenius R p n) a
source
@[simp]
theorem coe_iterateFrobeniusEquiv (R : Type u_1) (p n : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
⇑(iterateFrobeniusEquiv R p n) = ⇑(iterateFrobenius R p n)
source
theorem iterateFrobeniusEquiv_def (R : Type u_1) (p n : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) :
(iterateFrobeniusEquiv R p n) x = x ^ p ^ n
source
theorem iterateFrobeniusEquiv_add_apply (R : Type u_1) (p m n : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) :
(iterateFrobeniusEquiv R p (m + n)) x = (iterateFrobeniusEquiv R p m) ((iterateFrobeniusEquiv R p n) x)
source
theorem iterateFrobeniusEquiv_add (R : Type u_1) (p m n : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
iterateFrobeniusEquiv R p (m + n) = (iterateFrobeniusEquiv R p n).trans (iterateFrobeniusEquiv R p m)
source
theorem iterateFrobeniusEquiv_symm_add_apply (R : Type u_1) (p m n : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) :
(iterateFrobeniusEquiv R p (m + n)).symm x = (iterateFrobeniusEquiv R p m).symm ((iterateFrobeniusEquiv R p n).symm x)
source
theorem iterateFrobeniusEquiv_symm_add (R : Type u_1) (p m n : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
(iterateFrobeniusEquiv R p (m + n)).symm = (iterateFrobeniusEquiv R p n).symm.trans (iterateFrobeniusEquiv R p m).symm
source
theorem iterateFrobeniusEquiv_zero_apply (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) :
(iterateFrobeniusEquiv R p 0) x = x
source
theorem iterateFrobeniusEquiv_one_apply (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) :
(iterateFrobeniusEquiv R p 1) x = x ^ p
source
@[simp]
theorem iterateFrobeniusEquiv_zero (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
iterateFrobeniusEquiv R p 0 = RingEquiv.refl R
source
@[simp]
theorem iterateFrobeniusEquiv_one (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
iterateFrobeniusEquiv R p 1 = frobeniusEquiv R p
source
theorem iterateFrobeniusEquiv_eq_pow (R : Type u_1) (p n : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
iterateFrobeniusEquiv R p n = frobeniusEquiv R p ^ n
source
theorem iterateFrobeniusEquiv_symm (R : Type u_1) (p n : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
(iterateFrobeniusEquiv R p n).symm = (frobeniusEquiv R p).symm ^ n
source
@[simp]
theorem frobeniusEquiv_symm_apply_frobenius (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) :
(frobeniusEquiv R p).symm ((frobenius R p) x) = x
source
@[simp]
theorem frobenius_apply_frobeniusEquiv_symm (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) :
(frobenius R p) ((frobeniusEquiv R p).symm x) = x
source
@[simp]
theorem frobenius_comp_frobeniusEquiv_symm (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
(frobenius R p).comp ↑(frobeniusEquiv R p).symm = RingHom.id R
source
@[simp]
theorem frobeniusEquiv_symm_comp_frobenius (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
(↑(frobeniusEquiv R p).symm).comp (frobenius R p) = RingHom.id R
source
@[simp]
theorem coe_frobenius_comp_coe_frobeniusEquiv_symm (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
⇑(frobenius R p) ∘ ⇑(frobeniusEquiv R p).symm = id
source
@[simp]
theorem coe_frobeniusEquiv_symm_comp_coe_frobenius (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
⇑(frobeniusEquiv R p).symm ∘ ⇑(frobenius R p) = id
source
@[simp]
theorem frobeniusEquiv_symm_pow_p (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) :
(frobeniusEquiv R p).symm x ^ p = x
source
@[simp]
theorem iterate_frobeniusEquiv_symm_pow_p_pow (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) (n : ℕ) :
(⇑(frobeniusEquiv R p).symm)^[n] x ^ p ^ n = x
source
theorem MonoidHom.map_frobeniusEquiv_symm {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] (p : ℕ) [ExpChar R p] [PerfectRing R p] [ExpChar S p] [PerfectRing S p] (f : R →* S) (x : R) :
f ((frobeniusEquiv R p).symm x) = (frobeniusEquiv S p).symm (f x)

The `(frobeniusEquiv R p).symm` version of `MonoidHom.map_frobenius`. `(frobeniusEquiv R p).symm` commute with any monoid homomorphisms.

source
theorem RingHom.map_frobeniusEquiv_symm {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] (p : ℕ) [ExpChar R p] [PerfectRing R p] [ExpChar S p] [PerfectRing S p] (f : R →+* S) (x : R) :
f ((frobeniusEquiv R p).symm x) = (frobeniusEquiv S p).symm (f x)
source
theorem MonoidHom.map_iterate_frobeniusEquiv_symm {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] (p : ℕ) [ExpChar R p] [PerfectRing R p] [ExpChar S p] [PerfectRing S p] (f : R →* S) (n : ℕ) (x : R) :
f ((⇑(frobeniusEquiv R p).symm)^[n] x) = (⇑(frobeniusEquiv S p).symm)^[n] (f x)
source
theorem RingHom.map_iterate_frobeniusEquiv_symm {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] (p : ℕ) [ExpChar R p] [PerfectRing R p] [ExpChar S p] [PerfectRing S p] (f : R →+* S) (n : ℕ) (x : R) :
f ((⇑(frobeniusEquiv R p).symm)^[n] x) = (⇑(frobeniusEquiv S p).symm)^[n] (f x)
source
theorem injective_pow_p (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] {x y : R} (h : x ^ p = y ^ p) :
x = y
source
theorem polynomial_expand_eq (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (f : Polynomial R) :
(Polynomial.expand R p) f = Polynomial.map (↑(frobeniusEquiv R p).symm) f ^ p
source
@[simp]
theorem not_irreducible_expand (R : Type u_2) (p : ℕ) [CommSemiring R] [Fact (Nat.Prime p)] [CharP R p] [PerfectRing R p] (f : Polynomial R) :
¬Irreducible ((Polynomial.expand R p) f)
source
instance instPerfectRingProd (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (S : Type u_2) [CommSemiring S] [ExpChar S p] [PerfectRing S p] :
PerfectRing (R × S) p
source
class PerfectField (K : Type u_1) [Field K] :
Prop

A perfect field.

See also `PerfectRing` for a generalisation in positive characteristic.

- separable_of_irreducible {f : Polynomial K} : Irreducible f → f.Separable

  A field is perfect if every irreducible polynomial is separable.

Instances

source
theorem PerfectRing.toPerfectField (K : Type u_1) (p : ℕ) [Field K] [ExpChar K p] [PerfectRing K p] :
PerfectField K
source
instance PerfectField.ofCharZero {K : Type u_1} [Field K] [CharZero K] :
PerfectField K
source
instance PerfectField.ofFinite {K : Type u_1} [Field K] [Finite K] :
PerfectField K
source
instance PerfectField.toPerfectRing {K : Type u_1} [Field K] [PerfectField K] (p : ℕ) [hp : ExpChar K p] :
PerfectRing K p

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

source
theorem PerfectField.separable_iff_squarefree {K : Type u_1} [Field K] [PerfectField K] {g : Polynomial K} :
g.Separable ↔ Squarefree g
source
instance Algebra.IsAlgebraic.isSeparable_of_perfectField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [PerfectField K] :
Algebra.IsSeparable K L

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

source
theorem Algebra.IsAlgebraic.perfectField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [PerfectField K] :
PerfectField L

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

source
theorem Polynomial.roots_expand_pow_map_iterateFrobenius_le {R : Type u_1} [CommRing R] [IsDomain R] (p n : ℕ) [ExpChar R p] (f : Polynomial R) :
Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots ≤ p ^ n • f.roots
source
theorem Polynomial.roots_expand_map_frobenius_le {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) :
Multiset.map (⇑(frobenius R p)) ((expand R p) f).roots ≤ p • f.roots
source
theorem Polynomial.roots_expand_pow_image_iterateFrobenius_subset {R : Type u_1} [CommRing R] [IsDomain R] (p n : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] :
Finset.image (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots.toFinset ⊆ f.roots.toFinset
source
theorem Polynomial.roots_expand_image_frobenius_subset {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] :
Finset.image (⇑(frobenius R p)) ((expand R p) f).roots.toFinset ⊆ f.roots.toFinset
source
theorem Polynomial.roots_expand_pow {R : Type u_1} [CommRing R] [IsDomain R] {p n : ℕ} [ExpChar R p] {f : Polynomial R} [PerfectRing R p] :
((expand R (p ^ n)) f).roots = p ^ n • Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) f.roots
source
theorem Polynomial.roots_expand {R : Type u_1} [CommRing R] [IsDomain R] {p : ℕ} [ExpChar R p] {f : Polynomial R} [PerfectRing R p] :
((expand R p) f).roots = p • Multiset.map (⇑(frobeniusEquiv R p).symm) f.roots
source
theorem Polynomial.roots_X_pow_char_pow_sub_C {R : Type u_1} [CommRing R] [IsDomain R] {p n : ℕ} [ExpChar R p] [PerfectRing R p] {y : R} :
(X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}
source
theorem Polynomial.roots_X_pow_char_pow_sub_C_pow {R : Type u_1} [CommRing R] [IsDomain R] {p n : ℕ} [ExpChar R p] [PerfectRing R p] {y : R} {m : ℕ} :
((X ^ p ^ n - C y) ^ m).roots = (m * p ^ n) • {(iterateFrobeniusEquiv R p n).symm y}
source
theorem Polynomial.roots_X_pow_char_sub_C {R : Type u_1} [CommRing R] [IsDomain R] {p : ℕ} [ExpChar R p] [PerfectRing R p] {y : R} :
(X ^ p - C y).roots = p • {(frobeniusEquiv R p).symm y}
source
theorem Polynomial.roots_X_pow_char_sub_C_pow {R : Type u_1} [CommRing R] [IsDomain R] {p : ℕ} [ExpChar R p] [PerfectRing R p] {y : R} {m : ℕ} :
((X ^ p - C y) ^ m).roots = (m * p) • {(frobeniusEquiv R p).symm y}
source
theorem Polynomial.roots_expand_pow_map_iterateFrobenius {R : Type u_1} [CommRing R] [IsDomain R] {p n : ℕ} [ExpChar R p] {f : Polynomial R} [PerfectRing R p] :
Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots = p ^ n • f.roots
source
theorem Polynomial.roots_expand_map_frobenius {R : Type u_1} [CommRing R] [IsDomain R] {p : ℕ} [ExpChar R p] {f : Polynomial R} [PerfectRing R p] :
Multiset.map (⇑(frobenius R p)) ((expand R p) f).roots = p • f.roots
source
theorem Polynomial.roots_expand_image_iterateFrobenius {R : Type u_1} [CommRing R] [IsDomain R] {p n : ℕ} [ExpChar R p] {f : Polynomial R} [PerfectRing R p] [DecidableEq R] :
Finset.image (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots.toFinset = f.roots.toFinset
source
theorem Polynomial.roots_expand_image_frobenius {R : Type u_1} [CommRing R] [IsDomain R] {p : ℕ} [ExpChar R p] {f : Polynomial R} [PerfectRing R p] [DecidableEq R] :
Finset.image (⇑(frobenius R p)) ((expand R p) f).roots.toFinset = f.roots.toFinset
source
noncomputable def Polynomial.rootsExpandToRoots {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] :
↥((expand R p) f).roots.toFinset ↪ ↥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

- Polynomial.rootsExpandToRoots p f = { toFun := fun (x : ↥((Polynomial.expand R p) f).roots.toFinset) => ⟨↑x ^ p, ⋯⟩, inj' := ⋯ }

Instances For

source
@[simp]
theorem Polynomial.rootsExpandToRoots_apply {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] (x : ↥((expand R p) f).roots.toFinset) :
↑((rootsExpandToRoots p f) x) = ↑x ^ p
source
noncomputable def Polynomial.rootsExpandPowToRoots {R : Type u_1} [CommRing R] [IsDomain R] (p n : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] :
↥((expand R (p ^ n)) f).roots.toFinset ↪ ↥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

- Polynomial.rootsExpandPowToRoots p n f = { toFun := fun (x : ↥((Polynomial.expand R (p ^ n)) f).roots.toFinset) => ⟨↑x ^ p ^ n, ⋯⟩, inj' := ⋯ }

Instances For

source
@[simp]
theorem Polynomial.rootsExpandPowToRoots_apply {R : Type u_1} [CommRing R] [IsDomain R] (p n : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] (x : ↥((expand R (p ^ n)) f).roots.toFinset) :
↑((rootsExpandPowToRoots p n f) x) = ↑x ^ p ^ n
source
noncomputable def Polynomial.rootsExpandEquivRoots {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] [PerfectRing R p] :
↥((expand R p) f).roots.toFinset ≃ ↥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

- Polynomial.rootsExpandEquivRoots p f = ((frobeniusEquiv R p).image ↑((Polynomial.expand R p) f).roots.toFinset).trans (Equiv.setCongr ⋯)

Instances For

source
@[simp]
theorem Polynomial.rootsExpandEquivRoots_apply {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] [PerfectRing R p] (x : ↥((expand R p) f).roots.toFinset) :
↑((rootsExpandEquivRoots p f) x) = ↑x ^ p
source
noncomputable def Polynomial.rootsExpandPowEquivRoots {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] [PerfectRing R p] (n : ℕ) :
↥((expand R (p ^ n)) f).roots.toFinset ≃ ↥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

- Polynomial.rootsExpandPowEquivRoots p f n = ((iterateFrobeniusEquiv R p n).image ↑((Polynomial.expand R (p ^ n)) f).roots.toFinset).trans (Equiv.setCongr ⋯)

Instances For

source
@[simp]
theorem Polynomial.rootsExpandPowEquivRoots_apply {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] [PerfectRing R p] (n : ℕ) (x : ↥((expand R (p ^ n)) f).roots.toFinset) :
↑((rootsExpandPowEquivRoots p f n) x) = ↑x ^ p ^ n