# Documentation

## References #

• [Hazewinkel, Witt Vectors][Haze09]

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

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

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) }
Instances For
theorem WittVector.verschiebungFun_coeff {p : } {R : Type u_1} [] (x : ) (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} [] (x : ) :
x.verschiebungFun.coeff 0 = 0
@[simp]
theorem WittVector.verschiebungFun_coeff_succ {p : } {R : Type u_1} [] (x : ) (n : ) :
x.verschiebungFun.coeff n.succ = x.coeff n
theorem WittVector.ghostComponent_zero_verschiebungFun {p : } {R : Type u_1} [hp : Fact p.Prime] [] (x : ) :
x.verschiebungFun = 0
theorem WittVector.ghostComponent_verschiebungFun {p : } {R : Type u_1} [hp : Fact p.Prime] [] (x : ) (n : ) :
() x.verschiebungFun = p *

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

Equations
Instances For
@[simp]
theorem WittVector.aeval_verschiebung_poly' {p : } {R : Type u_1} [] (x : ) (n : ) :
(MvPolynomial.aeval x.coeff) = x.verschiebungFun.coeff n
instance WittVector.verschiebungFun_isPoly (p : ) :
WittVector.IsPoly p fun (R : Type u_3) (_Rcr : ) => WittVector.verschiebungFun

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

Equations
• =
noncomputable def WittVector.verschiebung {p : } {R : Type u_1} [hp : Fact p.Prime] [] :

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' := }
Instances For
theorem WittVector.verschiebung_isPoly {p : } [hp : Fact p.Prime] :
WittVector.IsPoly p fun (R : Type u_3) (_Rcr : ) => WittVector.verschiebung

WittVector.verschiebung is a polynomial function.

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

verschiebung is a natural transformation

theorem WittVector.ghostComponent_zero_verschiebung {p : } {R : Type u_1} [hp : Fact p.Prime] [] (x : ) :
(WittVector.verschiebung x) = 0
theorem WittVector.ghostComponent_verschiebung {p : } {R : Type u_1} [hp : Fact p.Prime] [] (x : ) (n : ) :
() (WittVector.verschiebung x) = p *
@[simp]
theorem WittVector.verschiebung_coeff_zero {p : } {R : Type u_1} [hp : Fact p.Prime] [] (x : ) :
(WittVector.verschiebung x).coeff 0 = 0
theorem WittVector.verschiebung_coeff_add_one {p : } {R : Type u_1} [hp : Fact p.Prime] [] (x : ) (n : ) :
(WittVector.verschiebung x).coeff (n + 1) = x.coeff n
@[simp]
theorem WittVector.verschiebung_coeff_succ {p : } {R : Type u_1} [hp : Fact p.Prime] [] (x : ) (n : ) :
(WittVector.verschiebung x).coeff n.succ = x.coeff n
theorem WittVector.aeval_verschiebungPoly {p : } {R : Type u_1} [hp : Fact p.Prime] [] (x : ) (n : ) :
(MvPolynomial.aeval x.coeff) = (WittVector.verschiebung x).coeff n
@[simp]
theorem WittVector.bind₁_verschiebungPoly_wittPolynomial {p : } [hp : Fact p.Prime] (n : ) :
= if n = 0 then 0 else p * wittPolynomial p (n - 1)