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 : ℕ) [Pow R ℕ] :

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 fun (x : R) => x ^ p
A ring is perfect if the Frobenius map is bijective.

Instances

source

instance one (M : Type u_1) [CommMonoid M] :

PerfectRing M 1

source

instance mul (M : Type u_1) (p q : ℕ) [CommMonoid M] [PerfectRing M p] [PerfectRing M q] :

PerfectRing M (p * q)

source

instance pow (M : Type u_1) (p : ℕ) [CommMonoid M] [PerfectRing M p] (n : ℕ) :

PerfectRing M (p ^ n)

source

noncomputable def powMulEquiv (M : Type u_1) (p : ℕ) [CommMonoid M] [PerfectRing M p] :

M ≃* M

The p-th power automorphism for a perfect monoid.

Equations

powMulEquiv M p = MulEquiv.ofBijective (powMonoidHom p) ⋯

Instances For

source

@[simp]

theorem powMulEquiv_apply (M : Type u_1) (p : ℕ) [CommMonoid M] [PerfectRing M p] (a : M) :

(powMulEquiv M p) a = a ^ p

source

@[simp]

theorem powMulEquiv_symm_pow_p (M : Type u_1) (p : ℕ) [CommMonoid M] [PerfectRing M p] (x : M) :

(powMulEquiv M p).symm x ^ p = x

source

@[simp]

theorem powMulEquiv_one (M : Type u_1) [CommMonoid M] :

powMulEquiv M 1 = MulEquiv.refl M

source

theorem powMulEquiv_mul (M : Type u_1) (p q : ℕ) [CommMonoid M] [PerfectRing M p] [PerfectRing M q] :

powMulEquiv M (p * q) = (powMulEquiv M p).trans (powMulEquiv M q)

source

theorem powMulEquiv_mul' (M : Type u_1) (p q : ℕ) [CommMonoid M] [PerfectRing M p] [PerfectRing M q] :

powMulEquiv M (p * q) = (powMulEquiv M q).trans (powMulEquiv M p)

source

theorem powMulEquiv_pow (M : Type u_1) (p : ℕ) [CommMonoid M] [PerfectRing M p] (n : ℕ) :

powMulEquiv M (p ^ n) = powMulEquiv M p ^ n

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 powMulEquiv_eq_toMulEquiv_frobeniusEquiv (R : Type u_1) (p : ℕ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :

powMulEquiv R p = (frobeniusEquiv R p).toMulEquiv

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

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

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

Documentation

Mathlib.FieldTheory.Perfect

Perfect fields and rings #

Main definitions / statements: #