mathlib3 documentation

ring_theory.witt_vector.init_tail

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 #

References #

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

noncomputable 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
Instances for witt_vector.select
noncomputable 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
@[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) :
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
noncomputable 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
noncomputable 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_nsmul {p : } [hp : fact (nat.prime p)] {R : Type u_1} [comm_ring R] (m : ) (x : witt_vector p R) (n : ) :
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 : ) :
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 : ) :
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.