The Verschiebung operator

References

• [Hazewinkel, Witt Vectors][Haze09]

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

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

verschiebungFun x shifts the coefficients of x up by one, by inserting 0 as the 0th coefficient. x.coeff i then becomes (verchiebungFun x).coeff (i + 1).

verschiebungFun is the underlying function of the additive monoid hom WittVector.verschiebung.

Equations

• x.verschiebungFun = { coeff := fun (n : ℕ) => if n = 0 then 0 else x.coeff (n - 1) }

theorem WittVector.verschiebungFun_coeff {p : ℕ} {R : Type u_1} [CommRing R] (x : WittVector p R) (n : ℕ) : x.verschiebungFun.coeff n = if n = 0 then 0 else x.coeff (n - 1)

theorem WittVector.verschiebungFun_coeff_zero {p : ℕ} {R : Type u_1} [CommRing R] (x : WittVector p R) : x.verschiebungFun.coeff 0 = 0

@[simp]

theorem WittVector.verschiebungFun_coeff_succ {p : ℕ} {R : Type u_1} [CommRing R] (x : WittVector p R) (n : ℕ) : x.verschiebungFun.coeff n.succ = x.coeff n

theorem WittVector.ghostComponent_zero_verschiebungFun {p : ℕ} {R : Type u_1} [CommRing R] [hp : Fact (Nat.Prime p)] (x : WittVector p R) : (ghostComponent 0) x.verschiebungFun = 0

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

def WittVector.verschiebungPoly (n : ℕ) : MvPolynomial ℕ ℤ

The 0th Verschiebung polynomial is 0. For n > 0, the nth Verschiebung polynomial is the variable X (n-1).

Equations

• WittVector.verschiebungPoly n = if n = 0 then 0 else MvPolynomial.X (n - 1)

@[simp]

theorem WittVector.verschiebungPoly_zero : verschiebungPoly 0 = 0

theorem WittVector.aeval_verschiebung_poly' {p : ℕ} {R : Type u_1} [CommRing R] (x : WittVector p R) (n : ℕ) : (MvPolynomial.aeval x.coeff) (verschiebungPoly n) = x.verschiebungFun.coeff n

instance WittVector.verschiebungFun_isPoly (p : ℕ) : IsPoly p fun (R : Type u_3) (_Rcr : CommRing R) => verschiebungFun

WittVector.verschiebung has polynomial structure given by WittVector.verschiebungPoly.

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

verschiebung x shifts the coefficients of x up by one, by inserting 0 as the 0th coefficient. x.coeff i then becomes (verchiebung x).coeff (i + 1).

This is an additive monoid hom with underlying function verschiebung_fun.

Equations

• WittVector.verschiebung = { toFun := WittVector.verschiebungFun, map_zero' := ⋯, map_add' := ⋯ }

theorem WittVector.verschiebung_isPoly {p : ℕ} [hp : Fact (Nat.Prime p)] : IsPoly p fun (x : Type u_3) (x_1 : CommRing x) => ⇑verschiebung

WittVector.verschiebung is a polynomial function.

@[simp]

theorem WittVector.map_verschiebung {p : ℕ} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [hp : Fact (Nat.Prime p)] (f : R →+* S) (x : WittVector p R) : (map f) (verschiebung x) = verschiebung ((map f) x)

verschiebung is a natural transformation

theorem WittVector.ghostComponent_zero_verschiebung {p : ℕ} {R : Type u_1} [CommRing R] [hp : Fact (Nat.Prime p)] (x : WittVector p R) : (ghostComponent 0) (verschiebung x) = 0

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

@[simp]

theorem WittVector.verschiebung_coeff_zero {p : ℕ} {R : Type u_1} [CommRing R] [hp : Fact (Nat.Prime p)] (x : WittVector p R) : (verschiebung x).coeff 0 = 0

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

@[simp]

theorem WittVector.verschiebung_coeff_succ {p : ℕ} {R : Type u_1} [CommRing R] [hp : Fact (Nat.Prime p)] (x : WittVector p R) (n : ℕ) : (verschiebung x).coeff n.succ = x.coeff n

theorem WittVector.verschiebung_injective (p : ℕ) (R : Type u_1) [CommRing R] [hp : Fact (Nat.Prime p)] : Function.Injective ⇑verschiebung

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

@[simp]

theorem WittVector.bind₁_verschiebungPoly_wittPolynomial {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) : (MvPolynomial.bind₁ verschiebungPoly) (wittPolynomial p ℤ n) = if n = 0 then 0 else ↑p * wittPolynomial p ℤ (n - 1)