mathlib documentation

ring_theory.witt_vector.init_tail

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 mv_polynomial.bind₁.

Main declarations

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

def witt_vector.select {p : } {R : Type u_1} [comm_ring R] (P : → Prop) (x : 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.

Equations
def witt_vector.select_poly (P : → Prop) (n : ) :

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
theorem witt_vector.coeff_select {p : } {R : Type u_1} [comm_ring R] (P : → Prop) (x : witt_vector p R) (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 Rwitt_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 Rwitt_vector p Rwitt_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) :

theorem witt_vector.coeff_add_of_disjoint {p : } [hp : fact (nat.prime p)] (n : ) {R : Type u_1} [comm_ring R] (x y : witt_vector p R) (h : ∀ (n : ), x.coeff n = 0 y.coeff n = 0) :
(x + y).coeff n = x.coeff n + y.coeff n

def witt_vector.init {p : } {R : Type u_1} [comm_ring R] (n : ) :

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
def witt_vector.tail {p : } {R : Type u_1} [comm_ring R] (n : ) :

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
@[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 : ) :

@[simp]
theorem witt_vector.init_init {p : } {R : Type u_1} [comm_ring R] (x : witt_vector p R) (n : ) :

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 : ) :

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 : ) :

theorem witt_vector.init_neg {p : } [hp : fact (nat.prime p)] {R : Type u_1} [comm_ring R] (x : witt_vector p R) (n : ) :

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 : ) :

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.