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} [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.

Equations

• WittVector.select P x = WittVector.mk p fun (n : ℕ) => if P n then x.coeff n else 0

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.

Equations

• WittVector.selectPoly P n = if P n then MvPolynomial.X n else 0

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

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.

Equations

• WittVector.init n = WittVector.select fun (i : ℕ) => i < n

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.

Equations

• WittVector.tail n = WittVector.select fun (i : ℕ) => n ≤ i

@[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.

Equations

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

@[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.