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.

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

Equations

• ⋯ = ⋯

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

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

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

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

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 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) = RingEquiv.trans (iterateFrobeniusEquiv R p n) (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) : (RingEquiv.symm (iterateFrobeniusEquiv R p (m + n))) x = (RingEquiv.symm (iterateFrobeniusEquiv R p m)) ((RingEquiv.symm (iterateFrobeniusEquiv R p n)) x)

theorem iterateFrobeniusEquiv_symm_add (R : Type u_1) (p : ℕ) (m : ℕ) (n : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] : RingEquiv.symm (iterateFrobeniusEquiv R p (m + n)) = RingEquiv.trans (RingEquiv.symm (iterateFrobeniusEquiv R p n)) (RingEquiv.symm (iterateFrobeniusEquiv R p m))

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] : RingEquiv.symm (iterateFrobeniusEquiv R p n) = RingEquiv.symm (frobeniusEquiv R p) ^ n

@[simp]

theorem frobeniusEquiv_symm_apply_frobenius (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) : (RingEquiv.symm (frobeniusEquiv R p)) ((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) ((RingEquiv.symm (frobeniusEquiv R p)) x) = x

@[simp]

theorem frobenius_comp_frobeniusEquiv_symm (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] : RingHom.comp (frobenius R p) ↑(RingEquiv.symm (frobeniusEquiv R p)) = RingHom.id R

@[simp]

theorem frobeniusEquiv_symm_comp_frobenius (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] : RingHom.comp (↑(RingEquiv.symm (frobeniusEquiv R p))) (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) : (RingEquiv.symm (frobeniusEquiv R p)) x ^ p = x

theorem injective_pow_p (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] {x : R} {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 (↑(RingEquiv.symm (frobeniusEquiv R p))) 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)

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

Equations

• ⋯ = ⋯

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 → Polynomial.Separable f

  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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

theorem Algebra.IsAlgebraic.isSeparable_of_perfectField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [PerfectField K] (halg : Algebra.IsAlgebraic K L) : 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] [PerfectField K] (halg : Algebra.IsAlgebraic K L) : 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.roots ((Polynomial.expand R (p ^ n)) f)) ≤ p ^ n • Polynomial.roots f

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

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

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

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.roots ((Polynomial.expand R (p ^ n)) f) = p ^ n • Multiset.map (⇑(RingEquiv.symm (iterateFrobeniusEquiv R p n))) (Polynomial.roots f)

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

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.roots (Polynomial.X ^ p ^ n - Polynomial.C y) = p ^ n • {(RingEquiv.symm (iterateFrobeniusEquiv R p n)) 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.roots ((Polynomial.X ^ p ^ n - Polynomial.C y) ^ m) = (m * p ^ n) • {(RingEquiv.symm (iterateFrobeniusEquiv R p n)) 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.roots (Polynomial.X ^ p - Polynomial.C y) = p • {(RingEquiv.symm (frobeniusEquiv R p)) 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.roots ((Polynomial.X ^ p - Polynomial.C y) ^ m) = (m * p) • {(RingEquiv.symm (frobeniusEquiv R p)) 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.roots ((Polynomial.expand R (p ^ n)) f)) = p ^ n • Polynomial.roots f

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

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

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

noncomputable def Polynomial.rootsExpandToRoots {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] : { x : R // x ∈ Multiset.toFinset (Polynomial.roots ((Polynomial.expand R p) f)) } ↪ { x : R // x ∈ Multiset.toFinset (Polynomial.roots f) }

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

• One or more equations did not get rendered due to their size.

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

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

• One or more equations did not get rendered due to their size.

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

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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Polynomial.rootsExpandEquivRoots_apply {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) [PerfectRing R p] [DecidableEq R] (x : { x : R // x ∈ Multiset.toFinset (Polynomial.roots ((Polynomial.expand R p) f)) }) : ↑((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) [PerfectRing R p] [DecidableEq R] (n : ℕ) : { x : R // x ∈ Multiset.toFinset (Polynomial.roots ((Polynomial.expand R (p ^ n)) f)) } ≃ { x : R // x ∈ Multiset.toFinset (Polynomial.roots f) }

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

• One or more equations did not get rendered due to their size.

@[simp]

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