mathlib documentation

ring_theory.witt_vector.verschiebung

The Verschiebung operator #

References #

def witt_vector.verschiebung_fun {p : } {R : Type u_1} [comm_ring R] (x : witt_vector p R) :

verschiebung_fun x shifts the coefficients of x up by one, by inserting 0 as the 0th coefficient. x.coeff i then becomes (verchiebung_fun x).coeff (i + 1).

verschiebung_fun is the underlying function of the additive monoid hom witt_vector.verschiebung.

Equations
theorem witt_vector.verschiebung_fun_coeff {p : } {R : Type u_1} [comm_ring R] (x : witt_vector p R) (n : ) :
x.verschiebung_fun.coeff n = ite (n = 0) 0 (x.coeff (n - 1))
theorem witt_vector.verschiebung_fun_coeff_zero {p : } {R : Type u_1} [comm_ring R] (x : witt_vector p R) :
@[simp]
theorem witt_vector.verschiebung_fun_coeff_succ {p : } {R : Type u_1} [comm_ring R] (x : witt_vector p R) (n : ) :

The 0th Verschiebung polynomial is 0. For n > 0, the nth Verschiebung polynomial is the variable X (n-1).

Equations
@[instance]
def witt_vector.verschiebung_fun_is_poly.comp₂_i (p : ) (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), witt_vector.verschiebung_fun) R _Rcr (f x y))
@[instance]
def witt_vector.verschiebung_fun_is_poly.comp_i (p : ) (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), witt_vector.verschiebung_fun) R _Rcr f)
def witt_vector.verschiebung {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] :

verschiebung x shifts the coefficients of x up by one, by inserting 0 as the 0th coefficient. x.coeff i then becomes (verchiebung x).coeff (i + 1).

This is a additive monoid hom with underlying function verschiebung_fun.

Equations
theorem witt_vector.verschiebung_is_poly {p : } [hp : fact (nat.prime p)] :

witt_vector.verschiebung is a polynomial function.

@[instance]
def witt_vector.verschiebung_is_poly.comp_i {p : } [hp : fact (nat.prime p)] (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), witt_vector.verschiebung) R _Rcr f)
@[instance]
def witt_vector.verschiebung_is_poly.comp₂_i {p : } [hp : fact (nat.prime p)] (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), witt_vector.verschiebung) R _Rcr (f x y))
@[simp]
theorem witt_vector.map_verschiebung {p : } {R : Type u_1} {S : Type u_2} [hp : fact (nat.prime p)] [comm_ring R] [comm_ring S] (f : R →+* S) (x : witt_vector p R) :

verschiebung is a natural transformation

@[simp]
theorem witt_vector.verschiebung_coeff_zero {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x : witt_vector p R) :
theorem witt_vector.verschiebung_coeff_add_one {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x : witt_vector p R) (n : ) :
@[simp]
theorem witt_vector.verschiebung_coeff_succ {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x : witt_vector p R) (n : ) :