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

🔶 coverage

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

📐 coverage

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

📐 coverage

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

PerfectRing R p

source

📐 coverage

@[simp]

theorem bijective_frobenius (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :

Function.Bijective ⇑(frobenius R p)

source

📐 coverage

theorem bijective_iterateFrobenius (R : Type u_1) (p n : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :

Function.Bijective ⇑(iterateFrobenius R p n)

source

📐 coverage

@[simp]

theorem injective_frobenius (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :

Function.Injective ⇑(frobenius R p)

source

📐 coverage

@[simp]

theorem surjective_frobenius (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :

Function.Surjective ⇑(frobenius R p)

source

🔸 coverage

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

Instances For

source

📐 coverage

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

📐 coverage

@[simp]

theorem coe_frobeniusEquiv (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :

⇑(frobeniusEquiv R p) = ⇑(frobenius R p)

source

📐 coverage

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

🔸 coverage

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

Instances For

source

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

theorem frobeniusEquiv_symm_pow (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) :

(frobeniusEquiv R p).symm (x ^ p) = x

Variant with · ^ p inside of frobeniusEquiv.

source

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

🔶 coverage

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

📐 coverage

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

PerfectField K

source

📐 coverage

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

PerfectField K

source

📐 coverage

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

PerfectField K

source

📐 coverage

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

📐 coverage

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

g.Separable ↔ Squarefree g

source

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

📐 coverage

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

🔸 coverage

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

Instances For

source

📐 coverage

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

🔸 coverage

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

Instances For

source

📐 coverage

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

🔸 coverage

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

Instances For

source

📐 coverage

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

🔸 coverage

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

Instances For

source

📐 coverage

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

Documentation

Mathlib.FieldTheory.Perfect

Perfect fields and rings #

Main definitions / statements: #