mathlib documentation

ring_theory.witt_vector.mul_p

Multiplication by n in the ring of Witt vectors #

In this file we show that multiplication by n in the ring of Witt vectors is a polynomial function. We then use this fact to show that the composition of Frobenius and Verschiebung is equal to multiplication by p.

Main declarations #

References #

def witt_vector.witt_mul_n (p : ) [hp : fact (nat.prime p)] :

witt_mul_n p n is the family of polynomials that computes the coefficients of x * n in terms of the coefficients of the Witt vector x.

Equations
theorem witt_vector.mul_n_coeff {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (n : ) (x : witt_vector p R) (k : ) :
@[instance]
def witt_vector.mul_n_is_poly.comp₂_i (p : ) [hp : fact (nat.prime p)] (n : ) (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), x * n) R _Rcr (f x y))
theorem witt_vector.mul_n_is_poly (p : ) [hp : fact (nat.prime p)] (n : ) :
witt_vector.is_poly p (λ (R : Type u_1) (_Rcr : comm_ring R) (x : witt_vector p R), x * n)

Multiplication by n is a polynomial function.

@[instance]
def witt_vector.mul_n_is_poly.comp_i (p : ) [hp : fact (nat.prime p)] (n : ) (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), x * n) R _Rcr f)