init and tail #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 mv_polynomial.bind₁.
Main declarations #
witt_vector.init n x: the firstncoefficients ofx, as a Witt vector. All coefficients at indices ≥nare 0.witt_vector.tail n x: the complementary part toinit. All coefficients at indices <nare 0, otherwise they are the same as inx.witt_vector.coeff_add_of_disjoint: ifxandyare Witt vectors such that for everynthen-th coefficient ofxor ofyis0, then the coefficients ofx + yare justx.coeff n + y.coeff n.
References #
noncomputable
def
witt_vector.select
{p : ℕ}
{R : Type u_1}
[comm_ring R]
(P : ℕ → Prop)
(x : witt_vector p R) :
witt_vector p R
witt_vector.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.
Instances for witt_vector.select
The polynomial that witnesses that witt_vector.select is a polynomial function.
select_poly n is X n if P n holds, and 0 otherwise.
Equations
- witt_vector.select_poly P n = ite (P n) (mv_polynomial.X n) 0
theorem
witt_vector.coeff_select
{p : ℕ}
{R : Type u_1}
[comm_ring R]
(P : ℕ → Prop)
(x : witt_vector p R)
(n : ℕ) :
(witt_vector.select P x).coeff n = ⇑(mv_polynomial.aeval x.coeff) (witt_vector.select_poly P n)
@[instance]
def
witt_vector.select_is_poly.comp_i
{p : ℕ}
(P : ℕ → Prop)
(f : Π ⦃R : Type u_1⦄ [_inst_3 : comm_ring R], witt_vector p R → witt_vector p R)
[hf : witt_vector.is_poly p f] :
witt_vector.is_poly p (λ (R : Type u_1) (_Rcr : comm_ring R), (λ (R : Type u_1) (_Rcr : comm_ring R) (x : witt_vector p R), witt_vector.select P x) R _Rcr ∘ f)
@[instance]
def
witt_vector.select_is_poly.comp₂_i
{p : ℕ}
(P : ℕ → Prop)
(f : Π ⦃R : Type u_1⦄ [_inst_3 : comm_ring R], witt_vector p R → witt_vector p R → witt_vector p R)
[hf : witt_vector.is_poly₂ p f] :
witt_vector.is_poly₂ p (λ (R : Type u_1) (_Rcr : comm_ring R) (x y : witt_vector p R), (λ (R : Type u_1) (_Rcr : comm_ring R) (x : witt_vector p R), witt_vector.select P x) R _Rcr (f x y))
theorem
witt_vector.select_is_poly
{p : ℕ}
(P : ℕ → Prop) :
witt_vector.is_poly p (λ (R : Type u_1) (_Rcr : comm_ring R) (x : witt_vector p R), witt_vector.select P x)
theorem
witt_vector.select_add_select_not
{p : ℕ}
[hp : fact (nat.prime p)]
{R : Type u_1}
[comm_ring R]
(P : ℕ → Prop)
(x : witt_vector p R) :
witt_vector.select P x + witt_vector.select (λ (i : ℕ), ¬P i) x = x
noncomputable
def
witt_vector.init
{p : ℕ}
{R : Type u_1}
[comm_ring R]
(n : ℕ) :
witt_vector p R → witt_vector p R
witt_vector.init n x is the Witt vector of which the first n coefficients are those from x
and all other coefficients are 0.
See witt_vector.tail for the complementary part.
Equations
- witt_vector.init n = witt_vector.select (λ (i : ℕ), i < n)
noncomputable
def
witt_vector.tail
{p : ℕ}
{R : Type u_1}
[comm_ring R]
(n : ℕ) :
witt_vector p R → witt_vector p R
witt_vector.tail n x is the Witt vector of which the first n coefficients are 0
and all other coefficients are those from x.
See witt_vector.init for the complementary part.
Equations
- witt_vector.tail n = witt_vector.select (λ (i : ℕ), n ≤ i)
@[simp]
theorem
witt_vector.init_add_tail
{p : ℕ}
[hp : fact (nat.prime p)]
{R : Type u_1}
[comm_ring R]
(x : witt_vector p R)
(n : ℕ) :
witt_vector.init n x + witt_vector.tail n x = x
@[simp]
theorem
witt_vector.init_init
{p : ℕ}
{R : Type u_1}
[comm_ring R]
(x : witt_vector p R)
(n : ℕ) :
witt_vector.init n (witt_vector.init n x) = witt_vector.init n x
theorem
witt_vector.init_add
{p : ℕ}
[hp : fact (nat.prime p)]
{R : Type u_1}
[comm_ring R]
(x y : witt_vector p R)
(n : ℕ) :
witt_vector.init n (x + y) = witt_vector.init n (witt_vector.init n x + witt_vector.init n y)
theorem
witt_vector.init_mul
{p : ℕ}
[hp : fact (nat.prime p)]
{R : Type u_1}
[comm_ring R]
(x y : witt_vector p R)
(n : ℕ) :
witt_vector.init n (x * y) = witt_vector.init n (witt_vector.init n x * witt_vector.init n y)
theorem
witt_vector.init_neg
{p : ℕ}
[hp : fact (nat.prime p)]
{R : Type u_1}
[comm_ring R]
(x : witt_vector p R)
(n : ℕ) :
witt_vector.init n (-x) = witt_vector.init n (-witt_vector.init n x)
theorem
witt_vector.init_sub
{p : ℕ}
[hp : fact (nat.prime p)]
{R : Type u_1}
[comm_ring R]
(x y : witt_vector p R)
(n : ℕ) :
witt_vector.init n (x - y) = witt_vector.init n (witt_vector.init n x - witt_vector.init n y)
theorem
witt_vector.init_nsmul
{p : ℕ}
[hp : fact (nat.prime p)]
{R : Type u_1}
[comm_ring R]
(m : ℕ)
(x : witt_vector p R)
(n : ℕ) :
witt_vector.init n (m • x) = witt_vector.init n (m • witt_vector.init n x)
theorem
witt_vector.init_zsmul
{p : ℕ}
[hp : fact (nat.prime p)]
{R : Type u_1}
[comm_ring R]
(m : ℤ)
(x : witt_vector p R)
(n : ℕ) :
witt_vector.init n (m • x) = witt_vector.init n (m • witt_vector.init n x)
theorem
witt_vector.init_pow
{p : ℕ}
[hp : fact (nat.prime p)]
{R : Type u_1}
[comm_ring R]
(m : ℕ)
(x : witt_vector p R)
(n : ℕ) :
witt_vector.init n (x ^ m) = witt_vector.init n (witt_vector.init n x ^ m)
theorem
witt_vector.init_is_poly
(p n : ℕ) :
witt_vector.is_poly p (λ (R : Type u_1) (_Rcr : comm_ring R), witt_vector.init n)
witt_vector.init n x is polynomial in the coefficients of x.