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 : ℕ) [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.

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.

theorem PerfectRing.ofFiniteOfIsReduced (p : ℕ) (R : Type u_2) [CommRing R] [ExpChar R p] [Finite R] [IsReduced R] : PerfectRing R p

@[simp]

theorem bijective_frobenius (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] : Function.Bijective ⇑(frobenius R p)

theorem bijective_iterateFrobenius (R : Type u_1) (p n : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] : Function.Bijective ⇑(iterateFrobenius R p n)

@[simp]

theorem injective_frobenius (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] : Function.Injective ⇑(frobenius R p)

@[simp]

theorem surjective_frobenius (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] : Function.Surjective ⇑(frobenius R p)

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

@[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

@[simp]

theorem coe_frobeniusEquiv (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] : ⇑(frobeniusEquiv R p) = ⇑(frobenius R p)

theorem frobeniusEquiv_def (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) : (frobeniusEquiv R p) x = x ^ p

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

@[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

@[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)

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

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)

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)

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)

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

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

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

@[simp]

theorem iterateFrobeniusEquiv_zero (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] : iterateFrobeniusEquiv R p 0 = RingEquiv.refl R

@[simp]

theorem iterateFrobeniusEquiv_one (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] : iterateFrobeniusEquiv R p 1 = frobeniusEquiv R p

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

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

@[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

@[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

@[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

@[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

@[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

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

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

@[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)

theorem 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

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.

theorem PerfectRing.toPerfectField (K : Type u_1) (p : ℕ) [Field K] [ExpChar K p] [PerfectRing K p] : PerfectField K

theorem PerfectField.ofCharZero {K : Type u_1} [Field K] [CharZero K] : PerfectField K

theorem PerfectField.ofFinite {K : Type u_1} [Field K] [Finite K] : PerfectField K

theorem PerfectField.toPerfectRing {K : Type u_1} [Field K] [PerfectField K] (p : ℕ) [ExpChar K p] : PerfectRing K p

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

theorem PerfectField.separable_iff_squarefree {K : Type u_1} [Field K] [PerfectField K] {g : Polynomial K} : g.Separable ↔ Squarefree g

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

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.

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)) ((Polynomial.expand R (p ^ n)) f).roots ≤ p ^ n • f.roots

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)) ((Polynomial.expand R p) f).roots ≤ p • f.roots

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)) ((Polynomial.expand R (p ^ n)) f).roots.toFinset ⊆ f.roots.toFinset

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)) ((Polynomial.expand R p) f).roots.toFinset ⊆ f.roots.toFinset

theorem Polynomial.roots_expand_pow {R : Type u_1} [CommRing R] [IsDomain R] {p n : ℕ} [ExpChar R p] {f : Polynomial R} [PerfectRing R p] : ((Polynomial.expand R (p ^ n)) f).roots = p ^ n • Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) f.roots

theorem Polynomial.roots_expand {R : Type u_1} [CommRing R] [IsDomain R] {p : ℕ} [ExpChar R p] {f : Polynomial R} [PerfectRing R p] : ((Polynomial.expand R p) f).roots = p • Multiset.map (⇑(frobeniusEquiv R p).symm) f.roots

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} : (Polynomial.X ^ p ^ n - Polynomial.C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}

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 : ℕ} : ((Polynomial.X ^ p ^ n - Polynomial.C y) ^ m).roots = (m * p ^ n) • {(iterateFrobeniusEquiv R p n).symm y}

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} : (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} [CommRing R] [IsDomain R] {p : ℕ} [ExpChar R p] [PerfectRing 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} [CommRing R] [IsDomain R] {p n : ℕ} [ExpChar R p] {f : Polynomial R} [PerfectRing R p] : 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} [CommRing R] [IsDomain R] {p : ℕ} [ExpChar R p] {f : Polynomial R} [PerfectRing R p] : Multiset.map (⇑(frobenius R p)) ((Polynomial.expand R p) f).roots = p • f.roots

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)) ((Polynomial.expand R (p ^ n)) f).roots.toFinset = f.roots.toFinset

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)) ((Polynomial.expand R p) f).roots.toFinset = f.roots.toFinset

noncomputable def Polynomial.rootsExpandToRoots {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] : { x : R // x ∈ ((Polynomial.expand R p) 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

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

@[simp]

theorem Polynomial.rootsExpandToRoots_apply {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] (x : { x : R // x ∈ ((Polynomial.expand R p) f).roots.toFinset }) : ↑((Polynomial.rootsExpandToRoots p f) x) = ↑x ^ p

noncomputable def Polynomial.rootsExpandPowToRoots {R : Type u_1} [CommRing R] [IsDomain R] (p n : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] : { 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

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

@[simp]

theorem Polynomial.rootsExpandPowToRoots_apply {R : Type u_1} [CommRing R] [IsDomain R] (p n : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] (x : { x : R // x ∈ ((Polynomial.expand R (p ^ n)) f).roots.toFinset }) : ↑((Polynomial.rootsExpandPowToRoots p n f) x) = ↑x ^ p ^ n

noncomputable def Polynomial.rootsExpandEquivRoots {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] [PerfectRing R p] : { x : R // x ∈ ((Polynomial.expand R p) 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

• Polynomial.rootsExpandEquivRoots p f = ((frobeniusEquiv R p).image (Membership.mem ((Polynomial.expand R p) f).roots.toFinset.val)).trans (Equiv.Set.ofEq ⋯)

@[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 : { x : R // x ∈ ((Polynomial.expand R p) f).roots.toFinset }) : ↑((Polynomial.rootsExpandEquivRoots p f) x) = ↑x ^ p

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 : ℕ) : { 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

• Polynomial.rootsExpandPowEquivRoots p f n = ((iterateFrobeniusEquiv R p n).image (Membership.mem ((Polynomial.expand R (p ^ n)) f).roots.toFinset.val)).trans (Equiv.Set.ofEq ⋯)

@[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 : { x : R // x ∈ ((Polynomial.expand R (p ^ n)) f).roots.toFinset }) : ↑((Polynomial.rootsExpandPowEquivRoots p f n) x) = ↑x ^ p ^ n