Mathlib.FieldTheory.Perfect

PerfectRing structure

(R : Type*) (p : ℕ) [CommSemiring R] [ExpChar R p]

Full source

/-- 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). -/
class PerfectRing (R : Type*) (p : ℕ) [CommSemiring R] [ExpChar R p] : Prop where
  /-- A ring is perfect if the Frobenius map is bijective. -/
  bijective_frobenius : Bijective <| frobenius R p

Perfect Ring (Serre's sense)

Informal description

A commutative semiring $ R $ of characteristic $ p $ (a prime number) is called a *perfect ring* (in the sense of Serre) if the Frobenius endomorphism $ x \mapsto x^p $ is bijective.

PerfectRing.ofSurjective theorem

(R : Type*) (p : ℕ) [CommRing R] [ExpChar R p] [IsReduced R] (h : Surjective <| frobenius R p) : PerfectRing R p

Full source

/-- For a reduced ring, surjectivity of the Frobenius map is a sufficient condition for perfection.
-/
lemma PerfectRing.ofSurjective (R : Type*) (p : ℕ) [CommRing R] [ExpChar R p]
    [IsReduced R] (h : Surjective <| frobenius R p) : PerfectRing R p :=
  ⟨frobenius_inj R p, h⟩

Surjective Frobenius Implies Perfect Ring for Reduced Commutative Rings

Informal description

Let $ R $ be a commutative ring of characteristic $ p $ (a prime number) that is reduced (i.e., has no nonzero nilpotent elements). If the Frobenius endomorphism $ x \mapsto x^p $ is surjective, then $ R $ is a perfect ring in the sense of Serre.

PerfectRing.ofFiniteOfIsReduced instance

(R : Type*) [CommRing R] [ExpChar R p] [Finite R] [IsReduced R] : PerfectRing R p

Full source

instance PerfectRing.ofFiniteOfIsReduced (R : Type*) [CommRing R] [ExpChar R p]
    [Finite R] [IsReduced R] : PerfectRing R p :=
  ofSurjective _ _ <| Finite.surjective_of_injective (frobenius_inj R p)

Finite Reduced Commutative Rings are Perfect

Informal description

Every finite reduced commutative ring $ R $ of characteristic $ p $ (a prime number) is a perfect ring in the sense of Serre, meaning that the Frobenius endomorphism $ x \mapsto x^p $ is bijective.

bijective_frobenius theorem

: Bijective (frobenius R p)

Full source

@[simp]
theorem bijective_frobenius : Bijective (frobenius R p) := PerfectRing.bijective_frobenius

Bijectivity of Frobenius Endomorphism on Perfect Rings

Informal description

The Frobenius endomorphism $x \mapsto x^p$ on a perfect ring $R$ of characteristic $p$ is bijective.

bijective_iterateFrobenius theorem

: Bijective (iterateFrobenius R p n)

Full source

theorem bijective_iterateFrobenius : Bijective (iterateFrobenius R p n) :=
  coe_iterateFrobenius R p n ▸ (bijective_frobenius R p).iterate n

Bijectivity of Iterated Frobenius Endomorphism on Perfect Rings

Informal description

For any natural number $n$, the $n$-th iterate of the Frobenius endomorphism $x \mapsto x^p$ on a perfect ring $R$ of characteristic $p$ is bijective.

injective_frobenius theorem

: Injective (frobenius R p)

Full source

@[simp]
theorem injective_frobenius : Injective (frobenius R p) := (bijective_frobenius R p).1

Injectivity of Frobenius Endomorphism on Perfect Rings

Informal description

For a perfect ring $R$ of characteristic $p$, the Frobenius endomorphism $x \mapsto x^p$ is injective.

surjective_frobenius theorem

: Surjective (frobenius R p)

Full source

@[simp]
theorem surjective_frobenius : Surjective (frobenius R p) := (bijective_frobenius R p).2

Surjectivity of Frobenius Endomorphism on Perfect Rings

Informal description

The Frobenius endomorphism $x \mapsto x^p$ on a commutative semiring $R$ of characteristic $p$ is surjective.

frobeniusEquiv definition

: R ≃+* R

Full source

/-- The Frobenius automorphism for a perfect ring. -/
@[simps! apply]
noncomputable def frobeniusEquiv : R ≃+* R :=
  RingEquiv.ofBijective (frobenius R p) PerfectRing.bijective_frobenius

Frobenius Automorphism of a Perfect Ring

Informal description

The Frobenius automorphism for a perfect ring $ R $ of characteristic $ p $ is the ring isomorphism $ R \cong R $ given by $ x \mapsto x^p $.

coe_frobeniusEquiv theorem

: ⇑(frobeniusEquiv R p) = frobenius R p

Full source

@[simp]
theorem coe_frobeniusEquiv : ⇑(frobeniusEquiv R p) = frobenius R p := rfl

Frobenius Automorphism as Frobenius Endomorphism

Informal description

The underlying function of the Frobenius automorphism `frobeniusEquiv R p` is equal to the Frobenius endomorphism `frobenius R p`, i.e., for any element $x \in R$, we have $(frobeniusEquiv\, R\, p)(x) = x^p$.

frobeniusEquiv_def theorem

(x : R) : frobeniusEquiv R p x = x ^ p

Full source

theorem frobeniusEquiv_def (x : R) : frobeniusEquiv R p x = x ^ p := rfl

Frobenius Automorphism Evaluates to $x^p$

Informal description

For any element $x$ in a perfect ring $R$ of characteristic $p$, the Frobenius automorphism evaluated at $x$ equals $x$ raised to the power $p$, i.e., $\text{frobeniusEquiv}_R(p)(x) = x^p$.

iterateFrobeniusEquiv definition

: R ≃+* R

Full source

/-- The iterated Frobenius automorphism for a perfect ring. -/
@[simps! apply]
noncomputable def iterateFrobeniusEquiv : R ≃+* R :=
  RingEquiv.ofBijective (iterateFrobenius R p n) (bijective_iterateFrobenius R p n)

Iterated Frobenius automorphism on a perfect ring

Informal description

The $n$-th iterate of the Frobenius endomorphism $x \mapsto x^{p^n}$ on a perfect ring $R$ of characteristic $p$ is a ring automorphism (i.e., a bijective ring homomorphism from $R$ to itself).

coe_iterateFrobeniusEquiv theorem

: ⇑(iterateFrobeniusEquiv R p n) = iterateFrobenius R p n

Full source

@[simp]
theorem coe_iterateFrobeniusEquiv : ⇑(iterateFrobeniusEquiv R p n) = iterateFrobenius R p n := rfl

Equality of Iterated Frobenius Automorphism and Endomorphism

Informal description

The underlying function of the $n$-th iterate Frobenius automorphism on a perfect ring $R$ of characteristic $p$ is equal to the $n$-th iterate of the Frobenius endomorphism, i.e., $\text{iterateFrobeniusEquiv}_R(p,n)(x) = x^{p^n}$ for all $x \in R$.

iterateFrobeniusEquiv_def theorem

(x : R) : iterateFrobeniusEquiv R p n x = x ^ p ^ n

Full source

theorem iterateFrobeniusEquiv_def (x : R) : iterateFrobeniusEquiv R p n x = x ^ p ^ n := rfl

Frobenius Automorphism Power Identity: $\text{iterateFrobeniusEquiv}_R^p(n)(x) = x^{p^n}$

Informal description

For any element $x$ in a perfect ring $R$ of characteristic $p$ and any natural number $n$, the $n$-th iterate of the Frobenius automorphism evaluated at $x$ equals $x$ raised to the power $p^n$, i.e., $\text{iterateFrobeniusEquiv}_R^p(n)(x) = x^{p^n}$.

iterateFrobeniusEquiv_add_apply theorem

(x : R) : iterateFrobeniusEquiv R p (m + n) x = iterateFrobeniusEquiv R p m (iterateFrobeniusEquiv R p n x)

Full source

theorem iterateFrobeniusEquiv_add_apply (x : R) : iterateFrobeniusEquiv R p (m + n) x =
    iterateFrobeniusEquiv R p m (iterateFrobeniusEquiv R p n x) :=
  iterateFrobenius_add_apply R p m n x

Iterated Frobenius Automorphism Composition: $\text{Frob}^{m+n}(x) = \text{Frob}^m(\text{Frob}^n(x))$

Informal description

For any element $x$ in a perfect ring $R$ of characteristic $p$, the $(m + n)$-th iterate of the Frobenius automorphism applied to $x$ equals the $m$-th iterate of the Frobenius automorphism applied to the $n$-th iterate of the Frobenius automorphism applied to $x$. In symbols: \[ \text{Frob}^{m+n}(x) = \text{Frob}^m(\text{Frob}^n(x)) \] where $\text{Frob}^k$ denotes the $k$-th iterate of the Frobenius automorphism $x \mapsto x^p$ on $R$.

iterateFrobeniusEquiv_add theorem

: iterateFrobeniusEquiv R p (m + n) = (iterateFrobeniusEquiv R p n).trans (iterateFrobeniusEquiv R p m)

Full source

theorem iterateFrobeniusEquiv_add : iterateFrobeniusEquiv R p (m + n) =
    (iterateFrobeniusEquiv R p n).trans (iterateFrobeniusEquiv R p m) :=
  RingEquiv.ext (iterateFrobeniusEquiv_add_apply R p m n)

Composition of Iterated Frobenius Automorphisms: $\text{Frob}^{m+n} = \text{Frob}^n \circ \text{Frob}^m$

Informal description

For a perfect ring $R$ of characteristic $p$, the $(m + n)$-th iterate of the Frobenius automorphism is equal to the composition of the $n$-th iterate followed by the $m$-th iterate. In symbols: \[ \text{Frob}^{m+n} = \text{Frob}^n \circ \text{Frob}^m \] where $\text{Frob}^k$ denotes the $k$-th iterate of the Frobenius automorphism $x \mapsto x^p$ on $R$.

iterateFrobeniusEquiv_symm_add_apply theorem

 (x : R) :
  (iterateFrobeniusEquiv R p (m + n)).symm x = (iterateFrobeniusEquiv R p m).symm ((iterateFrobeniusEquiv R p n).symm x)

Full source

theorem iterateFrobeniusEquiv_symm_add_apply (x : R) : (iterateFrobeniusEquiv R p (m + n)).symm x =
    (iterateFrobeniusEquiv R p m).symm ((iterateFrobeniusEquiv R p n).symm x) :=
  (iterateFrobeniusEquiv R p (m + n)).injective <| by rw [RingEquiv.apply_symm_apply, add_comm,
    iterateFrobeniusEquiv_add_apply, RingEquiv.apply_symm_apply, RingEquiv.apply_symm_apply]

Inverse Iterated Frobenius Automorphism Composition: $\text{Frob}^{-(m+n)}(x) = \text{Frob}^{-m}(\text{Frob}^{-n}(x))$

Informal description

For any element $x$ in a perfect ring $R$ of characteristic $p$, the inverse of the $(m + n)$-th iterate of the Frobenius automorphism applied to $x$ equals the inverse of the $m$-th iterate of the Frobenius automorphism applied to the inverse of the $n$-th iterate of the Frobenius automorphism applied to $x$. In symbols: \[ \text{Frob}^{-(m+n)}(x) = \text{Frob}^{-m}(\text{Frob}^{-n}(x)) \] where $\text{Frob}^{-k}$ denotes the inverse of the $k$-th iterate of the Frobenius automorphism $x \mapsto x^p$ on $R$.

iterateFrobeniusEquiv_symm_add theorem

 :
  (iterateFrobeniusEquiv R p (m + n)).symm = (iterateFrobeniusEquiv R p n).symm.trans (iterateFrobeniusEquiv R p m).symm

Full source

theorem iterateFrobeniusEquiv_symm_add : (iterateFrobeniusEquiv R p (m + n)).symm =
    (iterateFrobeniusEquiv R p n).symm.trans (iterateFrobeniusEquiv R p m).symm :=
  RingEquiv.ext (iterateFrobeniusEquiv_symm_add_apply R p m n)

Inverse Iterated Frobenius Automorphism Composition: $\text{Frob}^{-(m+n)} = \text{Frob}^{-n} \circ \text{Frob}^{-m}$

Informal description

For a perfect ring $R$ of characteristic $p$, the inverse of the $(m + n)$-th iterate of the Frobenius automorphism is equal to the composition of the inverses of the $n$-th and $m$-th iterates. In symbols: \[ \text{Frob}^{-(m+n)} = \text{Frob}^{-n} \circ \text{Frob}^{-m} \] where $\text{Frob}^{-k}$ denotes the inverse of the $k$-th iterate of the Frobenius automorphism $x \mapsto x^p$ on $R$.

iterateFrobeniusEquiv_zero_apply theorem

(x : R) : iterateFrobeniusEquiv R p 0 x = x

Full source

theorem iterateFrobeniusEquiv_zero_apply (x : R) : iterateFrobeniusEquiv R p 0 x = x := by
  rw [iterateFrobeniusEquiv_def, pow_zero, pow_one]

Identity Property of Zeroth Frobenius Automorphism: $\text{iterateFrobeniusEquiv}_R^p(0)(x) = x$

Informal description

For any element $x$ in a perfect ring $R$ of characteristic $p$, the zeroth iterate of the Frobenius automorphism acts as the identity function, i.e., $\text{iterateFrobeniusEquiv}_R^p(0)(x) = x$.

iterateFrobeniusEquiv_one_apply theorem

(x : R) : iterateFrobeniusEquiv R p 1 x = x ^ p

Full source

theorem iterateFrobeniusEquiv_one_apply (x : R) : iterateFrobeniusEquiv R p 1 x = x ^ p := by
  rw [iterateFrobeniusEquiv_def, pow_one]

First Iterate of Frobenius Automorphism: $\text{iterateFrobeniusEquiv}_R^p(1)(x) = x^p$

Informal description

For any element $x$ in a perfect ring $R$ of characteristic $p$, the first iterate of the Frobenius automorphism evaluated at $x$ equals $x$ raised to the power $p$, i.e., $\text{iterateFrobeniusEquiv}_R^p(1)(x) = x^p$.

iterateFrobeniusEquiv_zero theorem

: iterateFrobeniusEquiv R p 0 = RingEquiv.refl R

Full source

@[simp]
theorem iterateFrobeniusEquiv_zero : iterateFrobeniusEquiv R p 0 = RingEquiv.refl R :=
  RingEquiv.ext (iterateFrobeniusEquiv_zero_apply R p)

Zeroth Frobenius Automorphism is Identity

Informal description

For a perfect ring $R$ of characteristic $p$, the zeroth iterate of the Frobenius automorphism is equal to the identity ring automorphism on $R$, i.e., $\text{iterateFrobeniusEquiv}_R(p, 0) = \text{id}_R$.

iterateFrobeniusEquiv_one theorem

: iterateFrobeniusEquiv R p 1 = frobeniusEquiv R p

Full source

@[simp]
theorem iterateFrobeniusEquiv_one : iterateFrobeniusEquiv R p 1 = frobeniusEquiv R p :=
  RingEquiv.ext (iterateFrobeniusEquiv_one_apply R p)

First Iterate of Frobenius Automorphism Equals Frobenius Automorphism

Informal description

For a perfect ring $ R $ of characteristic $ p $, the first iterate of the Frobenius automorphism $ x \mapsto x^{p} $ is equal to the Frobenius automorphism itself, i.e., \[ \text{iterateFrobeniusEquiv}_R(p, 1) = \text{frobeniusEquiv}_R(p). \]

iterateFrobeniusEquiv_eq_pow theorem

: iterateFrobeniusEquiv R p n = frobeniusEquiv R p ^ n

Full source

theorem iterateFrobeniusEquiv_eq_pow : iterateFrobeniusEquiv R p n = frobeniusEquiv R p ^ n :=
  DFunLike.ext' <| show _ = ⇑(RingAut.toPerm _ _) by
    rw [map_pow, Equiv.Perm.coe_pow]; exact (pow_iterate p n).symm

Iterated Frobenius Automorphism as Power of Frobenius Automorphism: $ \text{iterateFrobeniusEquiv}_R(p, n) = (\text{frobeniusEquiv}_R(p))^n $

Informal description

For a perfect ring $ R $ of characteristic $ p $ and any natural number $ n $, the $ n $-th iterate of the Frobenius automorphism $ x \mapsto x^{p^n} $ is equal to the $ n $-th power of the Frobenius automorphism $ x \mapsto x^p $, i.e., $ \text{iterateFrobeniusEquiv}_R(p, n) = (\text{frobeniusEquiv}_R(p))^n $.

iterateFrobeniusEquiv_symm theorem

: (iterateFrobeniusEquiv R p n).symm = (frobeniusEquiv R p).symm ^ n

Full source

theorem iterateFrobeniusEquiv_symm :
    (iterateFrobeniusEquiv R p n).symm = (frobeniusEquiv R p).symm ^ n := by
  rw [iterateFrobeniusEquiv_eq_pow]; exact (inv_pow _ _).symm

Inverse of Iterated Frobenius Automorphism as Power of Inverse Frobenius Automorphism

Informal description

For a perfect ring $R$ of characteristic $p$ and any natural number $n$, the inverse of the $n$-th iterate of the Frobenius automorphism $x \mapsto x^{p^n}$ is equal to the $n$-th power of the inverse of the Frobenius automorphism $x \mapsto x^p$, i.e., $$(\text{iterateFrobeniusEquiv}_R(p, n))^{-1} = (\text{frobeniusEquiv}_R(p)^{-1})^n.$$

frobeniusEquiv_symm_apply_frobenius theorem

(x : R) : (frobeniusEquiv R p).symm (frobenius R p x) = x

Full source

@[simp]
theorem frobeniusEquiv_symm_apply_frobenius (x : R) :
    (frobeniusEquiv R p).symm (frobenius R p x) = x :=
  leftInverse_surjInv PerfectRing.bijective_frobenius x

Inverse Frobenius Automorphism Acts as Left Inverse: $\text{Frob}^{-1}(x^p) = x$

Informal description

For any element $x$ in a perfect ring $R$ of characteristic $p$, the inverse of the Frobenius automorphism applied to the Frobenius endomorphism of $x$ returns $x$, i.e., $\text{Frob}^{-1}(x^p) = x$.

frobenius_apply_frobeniusEquiv_symm theorem

(x : R) : frobenius R p ((frobeniusEquiv R p).symm x) = x

Full source

@[simp]
theorem frobenius_apply_frobeniusEquiv_symm (x : R) :
    frobenius R p ((frobeniusEquiv R p).symm x) = x :=
  surjInv_eq _ _

Frobenius Automorphism Inverse Property: $x^p = x$

Informal description

For any element $x$ in a perfect ring $R$ of characteristic $p$, applying the Frobenius endomorphism to the inverse of the Frobenius automorphism yields $x$, i.e., $x^p = x$ where $x$ is the inverse image under the Frobenius automorphism.

frobenius_comp_frobeniusEquiv_symm theorem

: (frobenius R p).comp (frobeniusEquiv R p).symm = RingHom.id R

Full source

@[simp]
theorem frobenius_comp_frobeniusEquiv_symm :
    (frobenius R p).comp (frobeniusEquiv R p).symm = RingHom.id R := by
  ext; simp

Frobenius Endomorphism Composed with Inverse Frobenius Automorphism is Identity

Informal description

For a perfect ring $R$ of characteristic $p$, the composition of the Frobenius endomorphism $x \mapsto x^p$ with the inverse of the Frobenius automorphism is equal to the identity ring homomorphism on $R$.

frobeniusEquiv_symm_comp_frobenius theorem

: ((frobeniusEquiv R p).symm : R →+* R).comp (frobenius R p) = RingHom.id R

Full source

@[simp]
theorem frobeniusEquiv_symm_comp_frobenius :
    ((frobeniusEquiv R p).symm : R →+* R).comp (frobenius R p) = RingHom.id R := by
  ext; simp

Inverse Frobenius Automorphism is Left Inverse: $\text{Frob}^{-1} \circ \text{Frob} = \text{id}_R$

Informal description

For a perfect ring $R$ of characteristic $p$, the composition of the inverse Frobenius automorphism with the Frobenius endomorphism is equal to the identity ring homomorphism on $R$, i.e., $\text{Frob}^{-1} \circ \text{Frob} = \text{id}_R$.

frobeniusEquiv_symm_pow_p theorem

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

Full source

@[simp]
theorem frobeniusEquiv_symm_pow_p (x : R) : ((frobeniusEquiv R p).symm x) ^ p = x :=
  frobenius_apply_frobeniusEquiv_symm R p x

Inverse Frobenius Power Identity: $(f^{-1}(x))^p = x$ in Perfect Rings

Informal description

For any element $x$ in a perfect ring $R$ of characteristic $p$, the $p$-th power of the inverse of the Frobenius automorphism applied to $x$ equals $x$, i.e., $(f^{-1}(x))^p = x$ where $f$ is the Frobenius automorphism $x \mapsto x^p$.

injective_pow_p theorem

{x y : R} (h : x ^ p = y ^ p) : x = y

Full source

theorem injective_pow_p {x y : R} (h : x ^ p = y ^ p) : x = y := (frobeniusEquiv R p).injective h

Injective $p$-th Power in Perfect Rings

Informal description

For any elements $x$ and $y$ in a perfect ring $R$ of characteristic $p$, if $x^p = y^p$, then $x = y$.

polynomial_expand_eq theorem

(f : R[X]) : expand R p f = (f.map (frobeniusEquiv R p).symm) ^ p

Full source

lemma polynomial_expand_eq (f : R[X]) :
    expand R p f = (f.map (frobeniusEquiv R p).symm) ^ p := by
  rw [← (f.map (S := R) (frobeniusEquiv R p).symm).expand_char p, map_expand, map_map,
    frobenius_comp_frobeniusEquiv_symm, map_id]

Polynomial Expansion Formula in Perfect Rings: $\text{expand}_R^p f = (f \circ \varphi^{-1})^p$

Informal description

For any polynomial $f$ over a perfect ring $R$ of characteristic $p$, the expansion of $f$ by $p$ is equal to the $p$-th power of $f$ composed with the inverse Frobenius automorphism, i.e., \[ \text{expand}_R^p f = \left(f \circ \varphi^{-1}\right)^p \] where $\varphi$ is the Frobenius automorphism $x \mapsto x^p$ on $R$.

not_irreducible_expand theorem

(R p) [CommSemiring R] [Fact p.Prime] [CharP R p] [PerfectRing R p] (f : R[X]) : ¬Irreducible (expand R p f)

Full source

@[simp]
theorem not_irreducible_expand (R p) [CommSemiring R] [Fact p.Prime] [CharP R p] [PerfectRing R p]
    (f : R[X]) : ¬ Irreducible (expand R p f) := by
  rw [polynomial_expand_eq]
  exact not_irreducible_pow (Fact.out : p.Prime).ne_one

Non-irreducibility of Polynomial Expansion in Perfect Rings

Informal description

Let $ R $ be a commutative semiring of characteristic $ p $ (where $ p $ is a prime) that is a perfect ring. For any polynomial $ f $ over $ R $, the expansion of $ f $ by $ p $ is not irreducible.

instPerfectRingProd instance

(S : Type*) [CommSemiring S] [ExpChar S p] [PerfectRing S p] : PerfectRing (R × S) p

Full source

instance instPerfectRingProd (S : Type*) [CommSemiring S] [ExpChar S p] [PerfectRing S p] :
    PerfectRing (R × S) p where
  bijective_frobenius := (bijective_frobenius R p).prodMap (bijective_frobenius S p)

Product of Perfect Rings is Perfect

Informal description

For any commutative semiring $S$ of characteristic $p$ that is a perfect ring, the product ring $R \times S$ is also a perfect ring.

PerfectField structure

(K : Type*) [Field K]

Full source

/-- A perfect field.

See also `PerfectRing` for a generalisation in positive characteristic. -/
class PerfectField (K : Type*) [Field K] : Prop where
  /-- A field is perfect if every irreducible polynomial is separable. -/
  separable_of_irreducible : ∀ {f : K[X]}, Irreducible f → f.Separable

Perfect Field

Informal description

A perfect field is a field $ K $ where every irreducible polynomial over $ K $ is separable. This means that in such a field, all algebraic extensions are separable, ensuring that the minimal polynomial of any algebraic element has no repeated roots in its splitting field.

PerfectRing.toPerfectField theorem

(K : Type*) (p : ℕ) [Field K] [ExpChar K p] [PerfectRing K p] : PerfectField K

Full source

lemma PerfectRing.toPerfectField (K : Type*) (p : ℕ)
    [Field K] [ExpChar K p] [PerfectRing K p] : PerfectField K := by
  obtain hp | ⟨hp⟩ := ‹ExpChar K p›
  · exact ⟨Irreducible.separable⟩
  refine PerfectField.mk fun hf ↦ ?_
  rcases separable_or p hf with h | ⟨-, g, -, rfl⟩
  · assumption
  · exfalso; revert hf; haveI := Fact.mk hp; simp

Perfect rings (Serre's sense) are perfect fields

Informal description

Let $K$ be a field of characteristic $p$ (a prime number) that is perfect in the sense of Serre (i.e., the Frobenius endomorphism $x \mapsto x^p$ is bijective). Then $K$ is a perfect field, meaning every irreducible polynomial over $K$ is separable.

PerfectField.ofCharZero instance

[CharZero K] : PerfectField K

Full source

instance ofCharZero [CharZero K] : PerfectField K := ⟨Irreducible.separable⟩

Fields of Characteristic Zero are Perfect

Informal description

Every field $K$ of characteristic zero is perfect.

PerfectField.ofFinite instance

[Finite K] : PerfectField K

Full source

instance ofFinite [Finite K] : PerfectField K := by
  obtain ⟨p, _instP⟩ := CharP.exists K
  have : Fact p.Prime := ⟨CharP.char_is_prime K p⟩
  exact PerfectRing.toPerfectField K p

Finite Fields are Perfect

Informal description

Every finite field $K$ is perfect.

PerfectField.toPerfectRing instance

(p : ℕ) [hp : ExpChar K p] : PerfectRing K p

Full source

/-- A perfect field of characteristic `p` (prime) is a perfect ring. -/
instance toPerfectRing (p : ℕ) [hp : ExpChar K p] : PerfectRing K p := by
  refine PerfectRing.ofSurjective _ _ fun y ↦ ?_
  rcases hp with _ | hp
  · simp [frobenius]
  rw [← not_forall_not]
  apply mt (X_pow_sub_C_irreducible_of_prime hp)
  apply mt separable_of_irreducible
  simp [separable_def, isCoprime_zero_right, isUnit_iff_degree_eq_zero,
    derivative_X_pow, degree_X_pow_sub_C hp.pos, hp.ne_zero]

Perfect Fields are Perfect Rings in Characteristic p

Informal description

For any perfect field $K$ of characteristic $p$ (a prime number), $K$ is a perfect ring in the sense of Serre, meaning the Frobenius endomorphism $x \mapsto x^p$ is bijective.

PerfectField.separable_iff_squarefree theorem

{g : K[X]} : g.Separable ↔ Squarefree g

Full source

theorem separable_iff_squarefree {g : K[X]} : g.Separable ↔ Squarefree g := by
  refine ⟨Separable.squarefree, fun sqf ↦ isCoprime_of_irreducible_dvd (sqf.ne_zero ·.1) ?_⟩
  rintro p (h : Irreducible p) ⟨q, rfl⟩ (dvd : p ∣ derivative (p * q))
  replace dvd : p ∣ q := by
    rw [derivative_mul, dvd_add_left (dvd_mul_right p _)] at dvd
    exact (separable_of_irreducible h).dvd_of_dvd_mul_left dvd
  exact (h.1 : ¬ IsUnit p) (sqf _ <| mul_dvd_mul_left _ dvd)

Separability and Squarefreeness in Perfect Fields: $g$ separable $\leftrightarrow$ $g$ squarefree

Informal description

For any polynomial $g$ over a perfect field $K$, $g$ is separable if and only if $g$ is squarefree.

Algebra.IsAlgebraic.isSeparable_of_perfectField instance

{K L : Type*} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [PerfectField K] : Algebra.IsSeparable K L

Full source

/-- If `L / K` is an algebraic extension, `K` is a perfect field, then `L / K` is separable. -/
instance Algebra.IsAlgebraic.isSeparable_of_perfectField {K L : Type*} [Field K] [Field L]
    [Algebra K L] [Algebra.IsAlgebraic K L] [PerfectField K] : Algebra.IsSeparable K L :=
  ⟨fun x ↦ PerfectField.separable_of_irreducible <|
    minpoly.irreducible (Algebra.IsIntegral.isIntegral x)⟩

Separability of Algebraic Extensions over Perfect Fields

Informal description

For any algebraic field extension $L/K$ where $K$ is a perfect field, the extension $L/K$ is separable. This means that every element of $L$ has a separable minimal polynomial over $K$.

Algebra.IsAlgebraic.perfectField theorem

{K L : Type*} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [PerfectField K] : PerfectField L

Full source

/-- If `L / K` is an algebraic extension, `K` is a perfect field, then so is `L`. -/
theorem Algebra.IsAlgebraic.perfectField {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L] [PerfectField K] : PerfectField L := ⟨fun {f} hf ↦ by
  obtain ⟨_, _, hi, h⟩ := hf.exists_dvd_monic_irreducible_of_isIntegral (K := K)
  exact (PerfectField.separable_of_irreducible hi).map |>.of_dvd h⟩

Perfectness is preserved under algebraic field extensions

Informal description

Let $K$ be a perfect field and $L$ be a field extension of $K$ that is algebraic over $K$. Then $L$ is also a perfect field.

Polynomial.roots_expand_pow_map_iterateFrobenius_le theorem

: (expand R (p ^ n) f).roots.map (iterateFrobenius R p n) ≤ p ^ n • f.roots

Full source

theorem roots_expand_pow_map_iterateFrobenius_le :
    (expand R (p ^ n) f).roots.map (iterateFrobenius R p n) ≤ p ^ n • f.roots := by
  classical
  refine le_iff_count.2 fun r ↦ ?_
  by_cases h : ∃ s, r = s ^ p ^ n
  · obtain ⟨s, rfl⟩ := h
    simp_rw [count_nsmul, count_roots, ← rootMultiplicity_expand_pow, ← count_roots, count_map,
      count_eq_card_filter_eq]
    exact card_le_card (monotone_filter_right _ fun _ h ↦ iterateFrobenius_inj R p n h)
  convert Nat.zero_le _
  simp_rw [count_map, card_eq_zero]
  exact ext' fun t ↦ count_zero t ▸ count_filter_of_neg fun h' ↦ h ⟨t, h'⟩

Frobenius Iterate and Roots of Expanded Polynomial: $\mathrm{map}\, (\mathrm{Frob}^n)\, (\mathrm{roots}\, (f^{(p^n)})) \leq p^n \cdot \mathrm{roots}\, f$

Informal description

Let $R$ be a commutative ring of prime characteristic $p$, and let $f$ be a polynomial over $R$. For any natural number $n$, the multiset of roots of the expanded polynomial $\mathrm{expand}_R(p^n, f)$, when mapped by the $n$-th iterate of the Frobenius endomorphism, is a submultiset of $p^n$ times the multiset of roots of $f$. That is, \[ \mathrm{map}\, (\mathrm{iterateFrobenius}_{R,p}^n)\, (\mathrm{roots}\, (\mathrm{expand}_R(p^n, f))) \leq p^n \cdot \mathrm{roots}\, f. \]

Polynomial.roots_expand_map_frobenius_le theorem

: (expand R p f).roots.map (frobenius R p) ≤ p • f.roots

Full source

theorem roots_expand_map_frobenius_le :
    (expand R p f).roots.map (frobenius R p) ≤ p • f.roots := by
  rw [← iterateFrobenius_one]
  convert ← roots_expand_pow_map_iterateFrobenius_le p 1 f <;> apply pow_one

Frobenius Map and Roots of Expanded Polynomial: $\mathrm{map}\, (\mathrm{Frob})\, (\mathrm{roots}\, (f^{(p)})) \leq p \cdot \mathrm{roots}\, f$

Informal description

Let $R$ be a commutative ring of prime characteristic $p$, and let $f$ be a polynomial over $R$. The multiset of roots of the expanded polynomial $\mathrm{expand}_R(p, f)$, when mapped by the Frobenius endomorphism, is a submultiset of $p$ times the multiset of roots of $f$. That is, \[ \mathrm{map}\, (\mathrm{Frob}_{R,p})\, (\mathrm{roots}\, (\mathrm{expand}_R(p, f))) \leq p \cdot \mathrm{roots}\, f. \]

Polynomial.roots_expand_pow_image_iterateFrobenius_subset theorem

[DecidableEq R] : (expand R (p ^ n) f).roots.toFinset.image (iterateFrobenius R p n) ⊆ f.roots.toFinset

Full source

theorem roots_expand_pow_image_iterateFrobenius_subset [DecidableEq R] :
    (expand R (p ^ n) f).roots.toFinset.image (iterateFrobenius R p n) ⊆ f.roots.toFinset := by
  rw [Finset.image_toFinset, ← (roots f).toFinset_nsmul _ (expChar_pow_pos R p n).ne',
    toFinset_subset]
  exact subset_of_le (roots_expand_pow_map_iterateFrobenius_le p n f)

Frobenius Iterate Maps Roots of Expanded Polynomial into Original Roots

Informal description

Let $R$ be a commutative ring of prime characteristic $p$, and let $f$ be a polynomial over $R$. For any natural number $n$, the image of the roots of the expanded polynomial $\mathrm{expand}_R(p^n, f)$ under the $n$-th iterate of the Frobenius endomorphism is a subset of the roots of $f$. That is, \[ \mathrm{image}\, (\mathrm{iterateFrobenius}_{R,p}^n)\, (\mathrm{toFinset}\, (\mathrm{roots}\, (\mathrm{expand}_R(p^n, f)))) \subseteq \mathrm{toFinset}\, (\mathrm{roots}\, f). \]

Polynomial.roots_expand_image_frobenius_subset theorem

[DecidableEq R] : (expand R p f).roots.toFinset.image (frobenius R p) ⊆ f.roots.toFinset

Full source

theorem roots_expand_image_frobenius_subset [DecidableEq R] :
    (expand R p f).roots.toFinset.image (frobenius R p) ⊆ f.roots.toFinset := by
  rw [← iterateFrobenius_one]
  convert ← roots_expand_pow_image_iterateFrobenius_subset p 1 f
  apply pow_one

Frobenius Maps Roots of Expanded Polynomial into Original Roots

Informal description

Let $R$ be a commutative ring of prime characteristic $p$, and let $f$ be a polynomial over $R$. The image of the roots of the expanded polynomial $\mathrm{expand}_R(p, f)$ under the Frobenius endomorphism is a subset of the roots of $f$. That is, \[ \mathrm{image}\, (\mathrm{Frob}_{R,p})\, (\mathrm{toFinset}\, (\mathrm{roots}\, (\mathrm{expand}_R(p, f)))) \subseteq \mathrm{toFinset}\, (\mathrm{roots}\, f). \]

Polynomial.roots_expand_pow theorem

: (expand R (p ^ n) f).roots = p ^ n • f.roots.map (iterateFrobeniusEquiv R p n).symm

Full source

theorem roots_expand_pow :
    (expand R (p ^ n) f).roots = p ^ n • f.roots.map (iterateFrobeniusEquiv R p n).symm := by
  classical
  refine ext' fun r ↦ ?_
  rw [count_roots, rootMultiplicity_expand_pow, ← count_roots, count_nsmul, count_map,
    count_eq_card_filter_eq]; congr; ext
  exact (iterateFrobeniusEquiv R p n).eq_symm_apply.symm

Roots of $p^n$-Expanded Polynomial over Perfect Ring

Informal description

Let $R$ be a perfect ring of characteristic $p$ and $f \in R[X]$ a polynomial. For any natural number $n$, the multiset of roots of the expanded polynomial $\mathrm{expand}_R(p^n, f)$ is equal to $p^n$ times the multiset obtained by applying the inverse of the $n$-th iterate of the Frobenius automorphism to each root of $f$. That is, \[ \mathrm{roots}(\mathrm{expand}_R(p^n, f)) = p^n \cdot \mathrm{map}\, (\mathrm{iterateFrobeniusEquiv}_R(p, n)^{-1})\, \mathrm{roots}(f). \]

Polynomial.roots_expand theorem

: (expand R p f).roots = p • f.roots.map (frobeniusEquiv R p).symm

Full source

theorem roots_expand : (expand R p f).roots = p • f.roots.map (frobeniusEquiv R p).symm := by
  conv_lhs => rw [← pow_one p, roots_expand_pow, iterateFrobeniusEquiv_eq_pow, pow_one]
  rfl

Roots of $p$-Expanded Polynomial over Perfect Ring: $\mathrm{roots}(\mathrm{expand}_R(p, f)) = p \cdot \mathrm{map}\, (\mathrm{Frob}^{-1})\, \mathrm{roots}(f)$

Informal description

Let $R$ be a perfect ring of characteristic $p$ and let $f \in R[X]$ be a polynomial. The multiset of roots of the expanded polynomial $\mathrm{expand}_R(p, f)$ is equal to $p$ times the multiset obtained by applying the inverse of the Frobenius automorphism to each root of $f$. That is, \[ \mathrm{roots}(\mathrm{expand}_R(p, f)) = p \cdot \mathrm{map}\, (\mathrm{frobeniusEquiv}_R(p)^{-1})\, \mathrm{roots}(f). \]

Polynomial.roots_X_pow_char_pow_sub_C theorem

{y : R} : (X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}

Full source

theorem roots_X_pow_char_pow_sub_C {y : R} :
    (X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y} := by
  have H := roots_expand_pow (p := p) (n := n) (f := X - C y)
  rwa [roots_X_sub_C, Multiset.map_singleton, map_sub, expand_X, expand_C] at H

Roots of $X^{p^n} - y$ over a perfect ring of characteristic $p$

Informal description

Let $R$ be a perfect ring of characteristic $p$ and let $y \in R$. For any natural number $n$, the multiset of roots of the polynomial $X^{p^n} - y$ is equal to $p^n$ times the singleton multiset containing the inverse image of $y$ under the $n$-th iterate of the Frobenius automorphism. That is, \[ \mathrm{roots}(X^{p^n} - y) = p^n \cdot \{(\mathrm{iterateFrobeniusEquiv}_R(p, n))^{-1}(y)\}. \]

Polynomial.roots_X_pow_char_pow_sub_C_pow theorem

{y : R} {m : ℕ} : ((X ^ p ^ n - C y) ^ m).roots = (m * p ^ n) • {(iterateFrobeniusEquiv R p n).symm y}

Full source

theorem roots_X_pow_char_pow_sub_C_pow {y : R} {m : ℕ} :
    ((X ^ p ^ n - C y) ^ m).roots = (m * p ^ n) • {(iterateFrobeniusEquiv R p n).symm y} := by
  rw [roots_pow, roots_X_pow_char_pow_sub_C, mul_smul]

Roots of $(X^{p^n} - y)^m$ over a perfect ring of characteristic $p$

Informal description

Let $R$ be a perfect ring of characteristic $p$ and let $y \in R$. For any natural numbers $n$ and $m$, the multiset of roots of the polynomial $(X^{p^n} - y)^m$ is equal to $m p^n$ times the singleton multiset containing the inverse image of $y$ under the $n$-th iterate of the Frobenius automorphism. That is, \[ \mathrm{roots}\big((X^{p^n} - y)^m\big) = m p^n \cdot \big\{(\mathrm{iterateFrobeniusEquiv}_R(p, n))^{-1}(y)\big\}. \]

Polynomial.roots_X_pow_char_sub_C theorem

{y : R} : (X ^ p - C y).roots = p • {(frobeniusEquiv R p).symm y}

Full source

theorem roots_X_pow_char_sub_C {y : R} :
    (X ^ p - C y).roots = p • {(frobeniusEquiv R p).symm y} := by
  have H := roots_X_pow_char_pow_sub_C (p := p) (n := 1) (y := y)
  rwa [pow_one, iterateFrobeniusEquiv_one] at H

Roots of $X^p - y$ over a perfect ring of characteristic $p$

Informal description

Let $R$ be a perfect ring of characteristic $p$ and let $y \in R$. The multiset of roots of the polynomial $X^p - y$ is equal to $p$ times the singleton multiset containing the inverse image of $y$ under the Frobenius automorphism. That is, \[ \mathrm{roots}(X^p - y) = p \cdot \{(\mathrm{frobeniusEquiv}_R(p))^{-1}(y)\}. \]

Polynomial.roots_X_pow_char_sub_C_pow theorem

{y : R} {m : ℕ} : ((X ^ p - C y) ^ m).roots = (m * p) • {(frobeniusEquiv R p).symm y}

Full source

theorem roots_X_pow_char_sub_C_pow {y : R} {m : ℕ} :
    ((X ^ p - C y) ^ m).roots = (m * p) • {(frobeniusEquiv R p).symm y} := by
  have H := roots_X_pow_char_pow_sub_C_pow (p := p) (n := 1) (y := y) (m := m)
  rwa [pow_one, iterateFrobeniusEquiv_one] at H

Roots of $(X^p - y)^m$ over a perfect ring of characteristic $p$

Informal description

Let $R$ be a perfect ring of characteristic $p$ and let $y \in R$. For any natural number $m$, the multiset of roots of the polynomial $(X^p - y)^m$ is equal to $m p$ times the singleton multiset containing the inverse image of $y$ under the Frobenius automorphism. That is, \[ \mathrm{roots}\big((X^p - y)^m\big) = m p \cdot \big\{(\mathrm{frobeniusEquiv}_R(p))^{-1}(y)\big\}. \]

Polynomial.roots_expand_pow_map_iterateFrobenius theorem

: (expand R (p ^ n) f).roots.map (iterateFrobenius R p n) = p ^ n • f.roots

Full source

theorem roots_expand_pow_map_iterateFrobenius :
    (expand R (p ^ n) f).roots.map (iterateFrobenius R p n) = p ^ n • f.roots := by
  simp_rw [← coe_iterateFrobeniusEquiv, roots_expand_pow, Multiset.map_nsmul,
    Multiset.map_map, comp_apply, RingEquiv.apply_symm_apply, map_id']

Frobenius Image of Roots of $p^n$-Expanded Polynomial Equals $p^n$-Scaled Original Roots

Informal description

Let $R$ be a perfect ring of characteristic $p$ and $f \in R[X]$ a polynomial. For any natural number $n$, the multiset obtained by applying the $n$-th iterate of the Frobenius endomorphism to each root of the expanded polynomial $\mathrm{expand}_R(p^n, f)$ is equal to $p^n$ times the multiset of roots of $f$. In symbols: \[ \mathrm{map}\, (\mathrm{iterateFrobenius}_R(p, n))\, \mathrm{roots}(\mathrm{expand}_R(p^n, f)) = p^n \cdot \mathrm{roots}(f). \]

Polynomial.roots_expand_map_frobenius theorem

: (expand R p f).roots.map (frobenius R p) = p • f.roots

Full source

theorem roots_expand_map_frobenius : (expand R p f).roots.map (frobenius R p) = p • f.roots := by
  simp [roots_expand, Multiset.map_nsmul]

Frobenius Image of Roots of $p$-Expanded Polynomial Equals $p$-Scaled Original Roots

Informal description

Let $R$ be a perfect ring of characteristic $p$ and let $f \in R[X]$ be a polynomial. The multiset obtained by applying the Frobenius endomorphism to each root of the expanded polynomial $\mathrm{expand}_R(p, f)$ is equal to $p$ times the multiset of roots of $f$. In symbols: \[ \mathrm{map}\, (\mathrm{frobenius}_R(p))\, \mathrm{roots}(\mathrm{expand}_R(p, f)) = p \cdot \mathrm{roots}(f). \]

Polynomial.roots_expand_image_iterateFrobenius theorem

[DecidableEq R] : (expand R (p ^ n) f).roots.toFinset.image (iterateFrobenius R p n) = f.roots.toFinset

Full source

theorem roots_expand_image_iterateFrobenius [DecidableEq R] :
    (expand R (p ^ n) f).roots.toFinset.image (iterateFrobenius R p n) = f.roots.toFinset := by
  rw [Finset.image_toFinset, roots_expand_pow_map_iterateFrobenius,
    (roots f).toFinset_nsmul _ (expChar_pow_pos R p n).ne']

Frobenius Image of Roots of $p^n$-Expanded Polynomial Equals Roots of Original Polynomial

Informal description

Let $R$ be a perfect ring of characteristic $p$ with decidable equality, and let $f \in R[X]$ be a polynomial. For any natural number $n$, the image of the roots of the expanded polynomial $\mathrm{expand}_R(p^n, f)$ under the $n$-th iterate of the Frobenius endomorphism is equal to the set of roots of $f$. In symbols: \[ \left\{ \mathrm{iterateFrobenius}_R(p, n)(x) \mid x \in \mathrm{roots}(\mathrm{expand}_R(p^n, f)) \right\} = \mathrm{roots}(f). \]

Polynomial.roots_expand_image_frobenius theorem

[DecidableEq R] : (expand R p f).roots.toFinset.image (frobenius R p) = f.roots.toFinset

Full source

theorem roots_expand_image_frobenius [DecidableEq R] :
    (expand R p f).roots.toFinset.image (frobenius R p) = f.roots.toFinset := by
  rw [Finset.image_toFinset, roots_expand_map_frobenius,
      (roots f).toFinset_nsmul _ (expChar_pos R p).ne']

Frobenius Image of Roots of $p$-Expanded Polynomial Equals Roots of Original Polynomial

Informal description

Let $R$ be a perfect ring of characteristic $p$ with decidable equality, and let $f \in R[X]$ be a polynomial. The image of the roots of the expanded polynomial $\mathrm{expand}_R(p, f)$ under the Frobenius endomorphism $x \mapsto x^p$ is equal to the set of roots of $f$. In symbols: \[ \{x^p \mid x \in \mathrm{roots}(\mathrm{expand}_R(p, f))\} = \mathrm{roots}(f). \]

Polynomial.rootsExpandToRoots definition

: (expand R p f).roots.toFinset ↪ f.roots.toFinset

Full source

/-- 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`. -/
noncomputable def rootsExpandToRoots : (expand R p f).roots.toFinset ↪ f.roots.toFinset where
  toFun x := ⟨x ^ p, roots_expand_image_frobenius_subset p f (Finset.mem_image_of_mem _ x.2)⟩
  inj' _ _ h := Subtype.ext (frobenius_inj R p <| Subtype.ext_iff.1 h)

Injective map from roots of expanded polynomial to roots of original polynomial

Informal description

Given a polynomial $ f $ over an integral domain $ R $ of characteristic $ p $, there is an injective function from the set of roots of $ \text{expand}_R(p, f) $ to the set of roots of $ f $. The function is defined by $ x \mapsto x^p $, where $ x $ is a root of $ \text{expand}_R(p, f) $.

Polynomial.rootsExpandToRoots_apply theorem

(x) : (rootsExpandToRoots p f x : R) = x ^ p

Full source

@[simp]
theorem rootsExpandToRoots_apply (x) : (rootsExpandToRoots p f x : R) = x ^ p := rfl

Image of Root under Expansion-to-Roots Map: $x \mapsto x^p$

Informal description

For any root $x$ of the expanded polynomial $\text{expand}_R(p, f)$, the image under the injective map $\text{rootsExpandToRoots}$ is given by $x^p$.

Polynomial.rootsExpandPowToRoots definition

: (expand R (p ^ n) f).roots.toFinset ↪ f.roots.toFinset

Full source

/-- 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`. -/
noncomputable def rootsExpandPowToRoots :
    (expand R (p ^ n) f).roots.toFinset ↪ f.roots.toFinset where
  toFun x := ⟨x ^ p ^ n,
    roots_expand_pow_image_iterateFrobenius_subset p n f (Finset.mem_image_of_mem _ x.2)⟩
  inj' _ _ h := Subtype.ext (iterateFrobenius_inj R p n <| Subtype.ext_iff.1 h)

Injective map from roots of $ p^n $-expanded polynomial to roots of original polynomial

Informal description

Given a polynomial $ f $ over an integral domain $ R $ of characteristic $ p $, there is an injective function from the set of roots of the expanded polynomial $ \text{expand}_R(p^n, f) $ to the set of roots of $ f $. The function is defined by $ x \mapsto x^{p^n} $, where $ x $ is a root of $ \text{expand}_R(p^n, f) $.

Polynomial.rootsExpandPowToRoots_apply theorem

(x) : (rootsExpandPowToRoots p n f x : R) = x ^ p ^ n

Full source

@[simp]
theorem rootsExpandPowToRoots_apply (x) : (rootsExpandPowToRoots p n f x : R) = x ^ p ^ n := rfl

Image of Root under $p^n$-Expansion-to-Roots Map: $x \mapsto x^{p^n}$

Informal description

For any root $x$ of the expanded polynomial $\text{expand}_R(p^n, f)$, the image under the injective map $\text{rootsExpandPowToRoots}$ is given by $x^{p^n}$.

Polynomial.rootsExpandEquivRoots definition

: (expand R p f).roots.toFinset ≃ f.roots.toFinset

Full source

/-- 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`. -/
noncomputable def rootsExpandEquivRoots : (expand R p f).roots.toFinset ≃ f.roots.toFinset :=
  ((frobeniusEquiv R p).image _).trans <| .setCongr <| show _ '' setOf (· ∈ _) = setOf (· ∈ _) by
    classical simp_rw [← roots_expand_image_frobenius (p := p) (f := f), Finset.mem_val,
      Finset.setOf_mem, Finset.coe_image, RingEquiv.toEquiv_eq_coe, EquivLike.coe_coe,
      frobeniusEquiv_apply]

Bijection between roots of expanded polynomial and original polynomial via Frobenius map

Informal description

Given a polynomial $ f $ over a perfect integral domain $ R $ of characteristic $ p $, there is a bijection between the set of roots of the expanded polynomial $ \text{expand}_R(p, f) $ and the set of roots of $ f $. The bijection is given by $ x \mapsto x^p $, where $ x $ is a root of $ \text{expand}_R(p, f) $.

Polynomial.rootsExpandEquivRoots_apply theorem

(x) : (rootsExpandEquivRoots p f x : R) = x ^ p

Full source

@[simp]
theorem rootsExpandEquivRoots_apply (x) : (rootsExpandEquivRoots p f x : R) = x ^ p := rfl

Image of Root under Frobenius Bijection: $ x \mapsto x^p $

Informal description

For a polynomial $ f $ over a perfect integral domain $ R $ of characteristic $ p $, and for any root $ x $ of the expanded polynomial $ \text{expand}_R(p, f) $, the image under the bijection $ \text{rootsExpandEquivRoots} $ is given by $ x^p $. That is, $ \text{rootsExpandEquivRoots}(x) = x^p $.

Polynomial.rootsExpandPowEquivRoots definition

(n : ℕ) : (expand R (p ^ n) f).roots.toFinset ≃ f.roots.toFinset

Full source

/-- 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`. -/
noncomputable def rootsExpandPowEquivRoots (n : ℕ) :
    (expand R (p ^ n) f).roots.toFinset ≃ f.roots.toFinset :=
  ((iterateFrobeniusEquiv R p n).image _).trans <|
    .setCongr <| show _ '' (setOf (· ∈ _)) = setOf (· ∈ _) by
    classical simp_rw [← roots_expand_image_iterateFrobenius (p := p) (f := f) (n := n),
      Finset.mem_val, Finset.setOf_mem, Finset.coe_image, RingEquiv.toEquiv_eq_coe,
      EquivLike.coe_coe, iterateFrobeniusEquiv_apply]

Bijection between roots of $ p^n $-expanded polynomial and original polynomial via $ p^n $-th power map

Informal description

For a polynomial $ f $ over a perfect integral domain $ R $ of characteristic $ p $, and for any natural number $ n $, there is a bijection between the set of roots of the expanded polynomial $ \text{expand}_R(p^n, f) $ and the set of roots of $ f $. The bijection is given by $ x \mapsto x^{p^n} $, where $ x $ is a root of $ \text{expand}_R(p^n, f) $.

Polynomial.rootsExpandPowEquivRoots_apply theorem

(n : ℕ) (x) : (rootsExpandPowEquivRoots p f n x : R) = x ^ p ^ n

Full source

@[simp]
theorem rootsExpandPowEquivRoots_apply (n : ℕ) (x) :
    (rootsExpandPowEquivRoots p f n x : R) = x ^ p ^ n := rfl

Image of Root under $ p^n $-th Power Bijection: $ x \mapsto x^{p^n} $

Informal description

For a polynomial $ f $ over a perfect integral domain $ R $ of characteristic $ p $, any natural number $ n $, and any root $ x $ of the expanded polynomial $ \text{expand}_R(p^n, f) $, the image under the bijection $ \text{rootsExpandPowEquivRoots} $ is given by $ x^{p^n} $. That is, $ \text{rootsExpandPowEquivRoots}(x) = x^{p^n} $.

Main definitions / statements: