mathlib3 documentation

ring_theory.witt_vector.mul_coeff

Leading terms of Witt vector multiplication #

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

The goal of this file is to study the leading terms of the formula for the n+1st coefficient of a product of Witt vectors x and y over a ring of characteristic p. We aim to isolate the n+1st coefficients of x and y, and express the rest of the product in terms of a function of the lower coefficients.

For most of this file we work with terms of type mv_polynomial (fin 2 × ℕ) ℤ. We will eventually evaluate them in k, but first we must take care of a calculation that needs to happen in characteristic 0.

Main declarations #

noncomputable def witt_vector.witt_poly_prod (p n : ) :
( i in range n, (y.coeff i)^(p^(n-i)) * p^i.val) *
  ( i in range n, (y.coeff i)^(p^(n-i)) * p^i.val)
Equations
noncomputable def witt_vector.witt_poly_prod_remainder (p : ) [hp : fact (nat.prime p)] (n : ) :

The "remainder term" of witt_vector.witt_poly_prod. See mul_poly_of_interest_aux2.

Equations
noncomputable def witt_vector.remainder (p n : ) :

remainder p n represents the remainder term from mul_poly_of_interest_aux3. witt_poly_prod p (n+1) will have variables up to n+1, but remainder will only have variables up to n.

Equations
noncomputable def witt_vector.poly_of_interest (p : ) [hp : fact (nat.prime p)] (n : ) :

This is the polynomial whose degree we want to get a handle on.

Equations
theorem witt_vector.mul_poly_of_interest_aux1 (p : ) [hp : fact (nat.prime p)] (n : ) :
(finset.range (n + 1)).sum (λ (i : ), p ^ i * witt_vector.witt_mul p i ^ p ^ (n - i)) = witt_vector.witt_poly_prod p n
theorem witt_vector.peval_poly_of_interest (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [comm_ring k] (n : ) (x y : witt_vector p k) :
witt_vector.peval (witt_vector.poly_of_interest p n) ![λ (i : ), x.coeff i, λ (i : ), y.coeff i] = (x * y).coeff (n + 1) + p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) - y.coeff (n + 1) * (finset.range (n + 1 + 1)).sum (λ (i : ), p ^ i * x.coeff i ^ p ^ (n + 1 - i)) - x.coeff (n + 1) * (finset.range (n + 1 + 1)).sum (λ (i : ), p ^ i * y.coeff i ^ p ^ (n + 1 - i))
theorem witt_vector.peval_poly_of_interest' (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [comm_ring k] [char_p k p] (n : ) (x y : witt_vector p k) :
witt_vector.peval (witt_vector.poly_of_interest p n) ![λ (i : ), x.coeff i, λ (i : ), y.coeff i] = (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)

The characteristic p version of peval_poly_of_interest

theorem witt_vector.nth_mul_coeff' (p : ) [hp : fact (nat.prime p)] (k : Type u_1) [comm_ring k] [char_p k p] (n : ) :
(f : truncated_witt_vector p (n + 1) k truncated_witt_vector p (n + 1) k k), (x y : witt_vector p k), f (witt_vector.truncate_fun (n + 1) x) (witt_vector.truncate_fun (n + 1) y) = (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
theorem witt_vector.nth_mul_coeff (p : ) [hp : fact (nat.prime p)] (k : Type u_1) [comm_ring k] [char_p k p] (n : ) :
(f : truncated_witt_vector p (n + 1) k truncated_witt_vector p (n + 1) k k), (x y : witt_vector p k), (x * y).coeff (n + 1) = x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) + f (witt_vector.truncate_fun (n + 1) x) (witt_vector.truncate_fun (n + 1) y)
noncomputable def witt_vector.nth_remainder (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [comm_ring k] [char_p k p] (n : ) :
(fin (n + 1) k) (fin (n + 1) k) k

Produces the "remainder function" of the n+1st coefficient, which does not depend on the n+1st coefficients of the inputs.

Equations
theorem witt_vector.nth_remainder_spec (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [comm_ring k] [char_p k p] (n : ) (x y : witt_vector p k) :
(x * y).coeff (n + 1) = x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) + witt_vector.nth_remainder p n (witt_vector.truncate_fun (n + 1) x) (witt_vector.truncate_fun (n + 1) y)