The Frobenius operator

If R has characteristic p, then there is a ring endomorphism frobenius R p that raises r : R to the power p. By applying WittVector.map to frobenius R p, we obtain a ring endomorphism 𝕎 R →+* 𝕎 R. It turns out that this endomorphism can be described by polynomials over ℤ that do not depend on R or the fact that it has characteristic p. In this way, we obtain a Frobenius endomorphism WittVector.frobeniusFun : 𝕎 R → 𝕎 R for every commutative ring R.

Unfortunately, the aforementioned polynomials can not be obtained using the machinery of wittStructureInt that was developed in StructurePolynomial.lean. We therefore have to define the polynomials by hand, and check that they have the required property.

In case R has characteristic p, we show in frobenius_eq_map_frobenius that WittVector.frobeniusFun is equal to WittVector.map (frobenius R p).

Main definitions and results

• frobeniusPoly: the polynomials that describe the coefficients of frobeniusFun;
• frobeniusFun: the Frobenius endomorphism on Witt vectors;
• frobeniusFun_isPoly: the tautological assertion that Frobenius is a polynomial function;
• frobenius_eq_map_frobenius: the fact that in characteristic p, Frobenius is equal to WittVector.map (frobenius R p).

TODO: Show that WittVector.frobeniusFun is a ring homomorphism, and bundle it into WittVector.frobenius.

References

• [Hazewinkel, Witt Vectors][Haze09]

• [Commelin and Lewis, Formalizing the Ring of Witt Vectors][CL21]

def WittVector.frobeniusPolyRat (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : MvPolynomial ℕ ℚ

The rational polynomials that give the coefficients of frobenius x, in terms of the coefficients of x. These polynomials actually have integral coefficients, see frobeniusPoly and map_frobeniusPoly.

Equations

• WittVector.frobeniusPolyRat p n = (MvPolynomial.bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) => n + 1)) (xInTermsOfW p ℚ n)

theorem WittVector.bind₁_frobeniusPolyRat_wittPolynomial (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : (MvPolynomial.bind₁ (WittVector.frobeniusPolyRat p)) (wittPolynomial p ℚ n) = wittPolynomial p ℚ (n + 1)

@[irreducible]

noncomputable def WittVector.frobeniusPolyAux (p : ℕ) : ℕ → MvPolynomial ℕ ℤ

An auxiliary polynomial over the integers, that satisfies p * (frobeniusPolyAux p n) + X n ^ p = frobeniusPoly p n. This makes it easy to show that frobeniusPoly p n is congruent to X n ^ p modulo p.

Equations

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

theorem WittVector.frobeniusPolyAux_eq (p : ℕ) (n : ℕ) : WittVector.frobeniusPolyAux p n = MvPolynomial.X (n + 1) - ∑ i ∈ Finset.range n, ∑ j ∈ Finset.range (p ^ (n - i)), (MvPolynomial.X i ^ p) ^ (p ^ (n - i) - (j + 1)) * WittVector.frobeniusPolyAux p i ^ (j + 1) * MvPolynomial.C ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - multiplicity p (j + 1)) * p ^ (j - multiplicity p (j + 1)))

def WittVector.frobeniusPoly (p : ℕ) (n : ℕ) : MvPolynomial ℕ ℤ

The polynomials that give the coefficients of frobenius x, in terms of the coefficients of x.

Equations

• WittVector.frobeniusPoly p n = MvPolynomial.X n ^ p + MvPolynomial.C ↑p * WittVector.frobeniusPolyAux p n

theorem WittVector.map_frobeniusPoly.key₁ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) (j : ℕ) (hj : j < p ^ n) : p ^ (n - multiplicity p (j + 1)) ∣ (p ^ n).choose (j + 1)

A key divisibility fact for the proof of WittVector.map_frobeniusPoly.

theorem WittVector.map_frobeniusPoly.key₂ (p : ℕ) [hp : Fact (Nat.Prime p)] {n : ℕ} {i : ℕ} {j : ℕ} (hi : i ≤ n) (hj : j < p ^ (n - i)) : j - multiplicity p (j + 1) + n = i + j + (n - i - multiplicity p (j + 1))

A key numerical identity needed for the proof of WittVector.map_frobeniusPoly.

theorem WittVector.map_frobeniusPoly (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : (MvPolynomial.map (Int.castRingHom ℚ)) (WittVector.frobeniusPoly p n) = WittVector.frobeniusPolyRat p n

theorem WittVector.frobeniusPoly_zmod (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : (MvPolynomial.map (Int.castRingHom (ZMod p))) (WittVector.frobeniusPoly p n) = MvPolynomial.X n ^ p

@[simp]

theorem WittVector.bind₁_frobeniusPoly_wittPolynomial (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : (MvPolynomial.bind₁ (WittVector.frobeniusPoly p)) (wittPolynomial p ℤ n) = wittPolynomial p ℤ (n + 1)

def WittVector.frobeniusFun {p : ℕ} {R : Type u_1} [CommRing R] (x : WittVector p R) : WittVector p R

frobeniusFun is the function underlying the ring endomorphism frobenius : 𝕎 R →+* frobenius 𝕎 R.

Equations

• x.frobeniusFun = WittVector.mk p fun (n : ℕ) => (MvPolynomial.aeval x.coeff) (WittVector.frobeniusPoly p n)

theorem WittVector.coeff_frobeniusFun {p : ℕ} {R : Type u_1} [CommRing R] (x : WittVector p R) (n : ℕ) : x.frobeniusFun.coeff n = (MvPolynomial.aeval x.coeff) (WittVector.frobeniusPoly p n)

instance WittVector.frobeniusFun_isPoly (p : ℕ) : WittVector.IsPoly p fun (R : Type u_2) (x : CommRing R) (Rcr : WittVector p R) => Rcr.frobeniusFun

frobeniusFun is tautologically a polynomial function.

See also frobenius_isPoly.

Equations

• ⋯ = ⋯

theorem WittVector.ghostComponent_frobeniusFun {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (n : ℕ) (x : WittVector p R) : (WittVector.ghostComponent n) x.frobeniusFun = (WittVector.ghostComponent (n + 1)) x

def WittVector.frobenius {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] : WittVector p R →+* WittVector p R

If R has characteristic p, then there is a ring endomorphism that raises r : R to the power p. By applying WittVector.map to this endomorphism, we obtain a ring endomorphism frobenius R p : 𝕎 R →+* 𝕎 R.

The underlying function of this morphism is WittVector.frobeniusFun.

Equations

• WittVector.frobenius = { toFun := WittVector.frobeniusFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem WittVector.coeff_frobenius {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x : WittVector p R) (n : ℕ) : (WittVector.frobenius x).coeff n = (MvPolynomial.aeval x.coeff) (WittVector.frobeniusPoly p n)

theorem WittVector.ghostComponent_frobenius {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (n : ℕ) (x : WittVector p R) : (WittVector.ghostComponent n) (WittVector.frobenius x) = (WittVector.ghostComponent (n + 1)) x

instance WittVector.frobenius_isPoly (p : ℕ) [hp : Fact (Nat.Prime p)] : WittVector.IsPoly p fun (R : Type u_2) (_Rcr : CommRing R) => ⇑WittVector.frobenius

frobenius is tautologically a polynomial function.

Equations

• ⋯ = ⋯

@[simp]

theorem WittVector.coeff_frobenius_charP (p : ℕ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] (x : WittVector p R) (n : ℕ) : (WittVector.frobenius x).coeff n = x.coeff n ^ p

theorem WittVector.frobenius_eq_map_frobenius (p : ℕ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] : WittVector.frobenius = WittVector.map (frobenius R p)

@[simp]

theorem WittVector.frobenius_zmodp (p : ℕ) [hp : Fact (Nat.Prime p)] (x : WittVector p (ZMod p)) : WittVector.frobenius x = x

@[simp]

theorem WittVector.frobeniusEquiv_symm_apply (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] [PerfectRing R p] : ⇑(WittVector.frobeniusEquiv p R).symm = ⇑(WittVector.map ↑(frobeniusEquiv R p).symm)

@[simp]

theorem WittVector.frobeniusEquiv_apply (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] [PerfectRing R p] : ⇑(WittVector.frobeniusEquiv p R) = ⇑WittVector.frobenius

def WittVector.frobeniusEquiv (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] [PerfectRing R p] : WittVector p R ≃+* WittVector p R

WittVector.frobenius as an equiv.

Equations

• WittVector.frobeniusEquiv p R = { toFun := ⇑WittVector.frobenius, invFun := ⇑(WittVector.map ↑(frobeniusEquiv R p).symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

theorem WittVector.frobenius_bijective (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] [PerfectRing R p] : Function.Bijective ⇑WittVector.frobenius