mathlib3 documentation

ring_theory.witt_vector.mul_p

Multiplication by n in the ring of Witt vectors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

source
noncomputable def witt_vector.witt_mul_n (p : ℕ) [hp : fact (nat.prime p)] :
ℕ → ℕ → mv_polynomial ℕ ℤ

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
source
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 : ℕ) :
(x * ↑n).coeff k = ⇑(mv_polynomial.aeval x.coeff) (witt_vector.witt_mul_n p n k)
source
@[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 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), x * ↑n) R _Rcr (f x y))
source
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.

source
@[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 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), x * ↑n) R _Rcr ∘ f)
source
@[simp]
theorem witt_vector.bind₁_witt_mul_n_witt_polynomial (p : ℕ) [hp : fact (nat.prime p)] (n k : ℕ) :
⇑(mv_polynomial.bind₁ (witt_vector.witt_mul_n p n)) (witt_polynomial p ℤ k) = ↑n * witt_polynomial p ℤ k