# Documentation

Mathlib.RingTheory.WittVector.MulCoeff

# Leading terms of Witt vector multiplication #

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 MvPolynomial (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 #

• WittVector.nth_mul_coeff: expresses the coefficient of a product of Witt vectors in terms of the previous coefficients of the multiplicands.
(∑ 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)

Instances For
theorem WittVector.wittPolyProd_vars (p : ) [hp : Fact ()] (n : ) :
Finset.univ ×ˢ Finset.range (n + 1)

The "remainder term" of WittVector.wittPolyProd. See mul_polyOfInterest_aux2.

Instances For
theorem WittVector.wittPolyProdRemainder_vars (p : ) [hp : Fact ()] (n : ) :
Finset.univ ×ˢ

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

Instances For
theorem WittVector.remainder_vars (p : ) [hp : Fact ()] (n : ) :
Finset.univ ×ˢ Finset.range (n + 1)
def WittVector.polyOfInterest (p : ) [hp : Fact ()] (n : ) :

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

Instances For
theorem WittVector.mul_polyOfInterest_aux1 (p : ) [hp : Fact ()] (n : ) :
(Finset.sum (Finset.range (n + 1)) fun i => p ^ i * ^ p ^ (n - i)) =
theorem WittVector.mul_polyOfInterest_aux2 (p : ) [hp : Fact ()] (n : ) :
p ^ n * + =
theorem WittVector.mul_polyOfInterest_aux3 (p : ) (n : ) :
WittVector.wittPolyProd p (n + 1) = -(p ^ (n + 1) * MvPolynomial.X (0, n + 1)) * (p ^ (n + 1) * MvPolynomial.X (1, n + 1)) + p ^ (n + 1) * MvPolynomial.X (0, n + 1) * ↑() (wittPolynomial p (n + 1)) + p ^ (n + 1) * MvPolynomial.X (1, n + 1) * ↑() (wittPolynomial p (n + 1)) +
theorem WittVector.mul_polyOfInterest_aux4 (p : ) [hp : Fact ()] (n : ) :
p ^ (n + 1) * WittVector.wittMul p (n + 1) = -(p ^ (n + 1) * MvPolynomial.X (0, n + 1)) * (p ^ (n + 1) * MvPolynomial.X (1, n + 1)) + p ^ (n + 1) * MvPolynomial.X (0, n + 1) * ↑() (wittPolynomial p (n + 1)) + p ^ (n + 1) * MvPolynomial.X (1, n + 1) * ↑() (wittPolynomial p (n + 1)) + ()
theorem WittVector.mul_polyOfInterest_aux5 (p : ) [hp : Fact ()] (n : ) :
p ^ (n + 1) * =
theorem WittVector.mul_polyOfInterest_vars (p : ) [hp : Fact ()] (n : ) :
MvPolynomial.vars (p ^ (n + 1) * ) Finset.univ ×ˢ Finset.range (n + 1)
theorem WittVector.polyOfInterest_vars_eq (p : ) [hp : Fact ()] (n : ) :
= MvPolynomial.vars (p ^ (n + 1) * (WittVector.wittMul p (n + 1) + p ^ (n + 1) * MvPolynomial.X (0, n + 1) * MvPolynomial.X (1, n + 1) - MvPolynomial.X (0, n + 1) * ↑() (wittPolynomial p (n + 1)) - MvPolynomial.X (1, n + 1) * ↑() (wittPolynomial p (n + 1))))
theorem WittVector.polyOfInterest_vars (p : ) [hp : Fact ()] (n : ) :
Finset.univ ×ˢ Finset.range (n + 1)
theorem WittVector.peval_polyOfInterest (p : ) [hp : Fact ()] {k : Type u_1} [] (n : ) (x : ) (y : ) :
WittVector.peval () ![fun i => , fun i => ] = (WittVector.coeff (x * y) (n + 1) + ↑(p ^ (n + 1)) * WittVector.coeff x (n + 1) * WittVector.coeff y (n + 1) - WittVector.coeff y (n + 1) * Finset.sum (Finset.range (n + 1 + 1)) fun i => ↑(p ^ i) * ^ p ^ (n + 1 - i)) - WittVector.coeff x (n + 1) * Finset.sum (Finset.range (n + 1 + 1)) fun i => ↑(p ^ i) * ^ p ^ (n + 1 - i)
theorem WittVector.peval_polyOfInterest' (p : ) [hp : Fact ()] {k : Type u_1} [] [CharP k p] (n : ) (x : ) (y : ) :
WittVector.peval () ![fun i => , fun i => ] = WittVector.coeff (x * y) (n + 1) - WittVector.coeff y (n + 1) * ^ p ^ (n + 1) - WittVector.coeff x (n + 1) * ^ p ^ (n + 1)

The characteristic p version of peval_polyOfInterest

theorem WittVector.nth_mul_coeff' (p : ) [hp : Fact ()] (k : Type u_1) [] [CharP k p] (n : ) :
f, ∀ (x y : ), f (WittVector.truncateFun (n + 1) x) (WittVector.truncateFun (n + 1) y) = WittVector.coeff (x * y) (n + 1) - WittVector.coeff y (n + 1) * ^ p ^ (n + 1) - WittVector.coeff x (n + 1) * ^ p ^ (n + 1)
theorem WittVector.nth_mul_coeff (p : ) [hp : Fact ()] (k : Type u_1) [] [CharP k p] (n : ) :
f, ∀ (x y : ), WittVector.coeff (x * y) (n + 1) = WittVector.coeff x (n + 1) * ^ p ^ (n + 1) + WittVector.coeff y (n + 1) * ^ p ^ (n + 1) + f (WittVector.truncateFun (n + 1) x) (WittVector.truncateFun (n + 1) y)
def WittVector.nthRemainder (p : ) [hp : Fact ()] {k : Type u_1} [] [CharP 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.

Instances For
theorem WittVector.nthRemainder_spec (p : ) [hp : Fact ()] {k : Type u_1} [] [CharP k p] (n : ) (x : ) (y : ) :
WittVector.coeff (x * y) (n + 1) = WittVector.coeff x (n + 1) * ^ p ^ (n + 1) + WittVector.coeff y (n + 1) * ^ p ^ (n + 1) + WittVector.nthRemainder p n (WittVector.truncateFun (n + 1) x) (WittVector.truncateFun (n + 1) y)