# init and tail#

Given a Witt vector x, we are sometimes interested in its components before and after an index n. This file defines those operations, proves that init is polynomial, and shows how that polynomial interacts with MvPolynomial.bind₁.

## Main declarations #

• WittVector.init n x: the first n coefficients of x, as a Witt vector. All coefficients at indices ≥ n are 0.
• WittVector.tail n x: the complementary part to init. All coefficients at indices < n are 0, otherwise they are the same as in x.
• WittVector.coeff_add_of_disjoint: if x and y are Witt vectors such that for every n the n-th coefficient of x or of y is 0, then the coefficients of x + y are just x.coeff n + y.coeff n.

## References #

• [Hazewinkel, Witt Vectors][Haze09]

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

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

WittVector.select P x, for a predicate P : ℕ → Prop is the Witt vector whose n-th coefficient is x.coeff n if P n is true, and 0 otherwise.

Equations
Instances For
def WittVector.selectPoly (P : ) (n : ) :

The polynomial that witnesses that WittVector.select is a polynomial function. selectPoly n is X n if P n holds, and 0 otherwise.

Equations
• = if P n then else 0
Instances For
theorem WittVector.coeff_select {p : } {R : Type u_1} [] (P : ) (x : ) (n : ) :
().coeff n = (MvPolynomial.aeval x.coeff) ()
instance WittVector.select_isPoly {p : } {P : } :
WittVector.IsPoly p fun (x : Type u_2) (x_1 : ) (x_2 : ) =>
Equations
• =
theorem WittVector.select_add_select_not {p : } [hp : Fact p.Prime] {R : Type u_1} [] (P : ) (x : ) :
+ WittVector.select (fun (i : ) => ¬P i) x = x
theorem WittVector.coeff_add_of_disjoint {p : } [hp : Fact p.Prime] (n : ) {R : Type u_1} [] (x : ) (y : ) (h : ∀ (n : ), x.coeff n = 0 y.coeff n = 0) :
(x + y).coeff n = x.coeff n + y.coeff n
def WittVector.init {p : } {R : Type u_1} [] (n : ) :

WittVector.init n x is the Witt vector of which the first n coefficients are those from x and all other coefficients are 0. See WittVector.tail for the complementary part.

Equations
Instances For
def WittVector.tail {p : } {R : Type u_1} [] (n : ) :

WittVector.tail n x is the Witt vector of which the first n coefficients are 0 and all other coefficients are those from x. See WittVector.init for the complementary part.

Equations
Instances For
@[simp]
theorem WittVector.init_add_tail {p : } [hp : Fact p.Prime] {R : Type u_1} [] (x : ) (n : ) :
+ = x

init_ring is an auxiliary tactic that discharges goals factoring init over ring operations.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem WittVector.init_init {p : } {R : Type u_1} [] (x : ) (n : ) :
=
theorem WittVector.init_add {p : } [hp : Fact p.Prime] {R : Type u_1} [] (x : ) (y : ) (n : ) :
theorem WittVector.init_mul {p : } [hp : Fact p.Prime] {R : Type u_1} [] (x : ) (y : ) (n : ) :
theorem WittVector.init_neg {p : } [hp : Fact p.Prime] {R : Type u_1} [] (x : ) (n : ) :
theorem WittVector.init_sub {p : } [hp : Fact p.Prime] {R : Type u_1} [] (x : ) (y : ) (n : ) :
theorem WittVector.init_nsmul {p : } [hp : Fact p.Prime] {R : Type u_1} [] (m : ) (x : ) (n : ) :
theorem WittVector.init_zsmul {p : } [hp : Fact p.Prime] {R : Type u_1} [] (m : ) (x : ) (n : ) :
theorem WittVector.init_pow {p : } [hp : Fact p.Prime] {R : Type u_1} [] (m : ) (x : ) (n : ) :
theorem WittVector.init_isPoly (p : ) (n : ) :
WittVector.IsPoly p fun (x : Type u_2) (x_1 : ) =>

WittVector.init n x is polynomial in the coefficients of x.