# mathlib3documentation

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 #

• witt_vector.nth_mul_coeff: expresses the coefficient of a product of Witt vectors in terms of the previous coefficients of the multiplicands.
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 * ^ p ^ (n - i)) =
theorem witt_vector.mul_poly_of_interest_aux3 (p n : ) :
(n + 1) = -(p ^ (n + 1) * mv_polynomial.X (0, n + 1)) * (p ^ (n + 1) * mv_polynomial.X (1, n + 1)) + p ^ (n + 1) * mv_polynomial.X (0, n + 1) * (n + 1)) + p ^ (n + 1) * mv_polynomial.X (1, n + 1) * (n + 1)) +
theorem witt_vector.mul_poly_of_interest_aux4 (p : ) [hp : fact (nat.prime p)] (n : ) :
p ^ (n + 1) * (n + 1) = -(p ^ (n + 1) * mv_polynomial.X (0, n + 1)) * (p ^ (n + 1) * mv_polynomial.X (1, n + 1)) + p ^ (n + 1) * mv_polynomial.X (0, n + 1) * (n + 1)) + p ^ (n + 1) * mv_polynomial.X (1, n + 1) * (n + 1)) + -
theorem witt_vector.mul_poly_of_interest_aux5 (p : ) [hp : fact (nat.prime p)] (n : ) :
p ^ (n + 1) * =
theorem witt_vector.poly_of_interest_vars_eq (p : ) [hp : fact (nat.prime p)] (n : ) :
= (p ^ (n + 1) * (n + 1) + p ^ (n + 1) * mv_polynomial.X (0, n + 1) * mv_polynomial.X (1, n + 1) - mv_polynomial.X (0, n + 1) * (n + 1)) - mv_polynomial.X (1, n + 1) * (n + 1)))).vars
theorem witt_vector.peval_poly_of_interest (p : ) [hp : fact (nat.prime p)] {k : Type u_1} [comm_ring k] (n : ) (x y : k) :
![λ (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] [ p] (n : ) (x y : k) :
![λ (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] [ p] (n : ) :
(f : (n + 1) k (n + 1) k k), (x y : 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] [ p] (n : ) :
(f : (n + 1) k (n + 1) k k), (x y : 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] [ 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] [ p] (n : ) (x y : 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.truncate_fun (n + 1) x) (witt_vector.truncate_fun (n + 1) y)