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]

noncomputable def WittVector.select {p : ℕ} {R : Type u_1} [CommRing R] (P : ℕ → Prop) (x : WittVector p R) : WittVector p R

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.

noncomputable def WittVector.selectPoly (P : ℕ → Prop) (n : ℕ) : MvPolynomial ℕ ℤ

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

theorem WittVector.coeff_select {p : ℕ} {R : Type u_1} [CommRing R] (P : ℕ → Prop) (x : WittVector p R) (n : ℕ) : (select P x).coeff n = (MvPolynomial.aeval x.coeff) (selectPoly P n)

instance WittVector.select_isPoly {p : ℕ} {P : ℕ → Prop} : IsPoly p fun (x : Type u_2) (x_1 : CommRing x) (x_2 : WittVector p x) => select P x_2

theorem WittVector.select_add_select_not {p : ℕ} {R : Type u_1} [CommRing R] (P : ℕ → Prop) [hp : Fact (Nat.Prime p)] (x : WittVector p R) : select P x + select (fun (i : ℕ) => ¬P i) x = x

theorem WittVector.coeff_add_of_disjoint {p : ℕ} (n : ℕ) {R : Type u_1} [CommRing R] [hp : Fact (Nat.Prime p)] (x y : WittVector p R) (h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0) : (x + y).coeff n = x.coeff n + y.coeff n

noncomputable def WittVector.init {p : ℕ} {R : Type u_1} [CommRing R] (n : ℕ) : WittVector p R → WittVector p R

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.

noncomputable def WittVector.tail {p : ℕ} {R : Type u_1} [CommRing R] (n : ℕ) : WittVector p R → WittVector p R

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.

@[simp]

theorem WittVector.init_add_tail {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (x : WittVector p R) (n : ℕ) : init n x + tail n x = x

def WittVector.initRing : Lean.ParserDescr

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

@[simp]

theorem WittVector.init_init {p : ℕ} {R : Type u_1} [CommRing R] (x : WittVector p R) (n : ℕ) : init n (init n x) = init n x

theorem WittVector.init_add {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (x y : WittVector p R) (n : ℕ) : init n (x + y) = init n (init n x + init n y)

theorem WittVector.init_mul {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (x y : WittVector p R) (n : ℕ) : init n (x * y) = init n (init n x * init n y)

theorem WittVector.init_neg {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (x : WittVector p R) (n : ℕ) : init n (-x) = init n (-init n x)

theorem WittVector.init_sub {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (x y : WittVector p R) (n : ℕ) : init n (x - y) = init n (init n x - init n y)

theorem WittVector.init_nsmul {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (m : ℕ) (x : WittVector p R) (n : ℕ) : init n (m • x) = init n (m • init n x)

theorem WittVector.init_zsmul {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (m : ℤ) (x : WittVector p R) (n : ℕ) : init n (m • x) = init n (m • init n x)

theorem WittVector.init_pow {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (m : ℕ) (x : WittVector p R) (n : ℕ) : init n (x ^ m) = init n (init n x ^ m)

theorem WittVector.init_isPoly (p n : ℕ) : IsPoly p fun (x : Type u_2) (x_1 : CommRing x) => init n

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