# 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 ∈ range n, (y.coeff i)^(p^(n-i)) * p^i.val) *
(∑ i ∈ range n, (y.coeff i)^(p^(n-i)) * p^i.val)

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

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

Equations
• = i ∈ , p ^ i * ^ p ^ (n - i)
Instances For
theorem WittVector.wittPolyProdRemainder_vars (p : ) [hp : Fact ()] (n : ) :
.vars 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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem WittVector.remainder_vars (p : ) [hp : Fact ()] (n : ) :
().vars 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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem WittVector.mul_polyOfInterest_aux1 (p : ) [hp : Fact ()] (n : ) :
iFinset.range (n + 1), 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 : ) :
(p ^ (n + 1) * ).vars Finset.univ ×ˢ Finset.range (n + 1)
theorem WittVector.polyOfInterest_vars_eq (p : ) [hp : Fact ()] (n : ) :
.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)))).vars
theorem WittVector.polyOfInterest_vars (p : ) [hp : Fact ()] (n : ) :
.vars Finset.univ ×ˢ Finset.range (n + 1)
theorem WittVector.peval_polyOfInterest (p : ) [hp : Fact ()] {k : Type u_1} [] (n : ) (x : ) (y : ) :
WittVector.peval ![fun (i : ) => x.coeff i, fun (i : ) => y.coeff i] = (x * y).coeff (n + 1) + p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) - y.coeff (n + 1) * iFinset.range (n + 1 + 1), p ^ i * x.coeff i ^ p ^ (n + 1 - i) - x.coeff (n + 1) * iFinset.range (n + 1 + 1), p ^ i * y.coeff 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 : ) => x.coeff i, fun (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_polyOfInterest

theorem WittVector.nth_mul_coeff' (p : ) [hp : Fact ()] (k : Type u_1) [] [CharP k p] (n : ) :
∃ (f : TruncatedWittVector p (n + 1) kTruncatedWittVector p (n + 1) kk), ∀ (x y : ), f (WittVector.truncateFun (n + 1) x) (WittVector.truncateFun (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 WittVector.nth_mul_coeff (p : ) [hp : Fact ()] (k : Type u_1) [] [CharP k p] (n : ) :
∃ (f : TruncatedWittVector p (n + 1) kTruncatedWittVector p (n + 1) kk), ∀ (x y : ), (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 (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.

Equations
Instances For
theorem WittVector.nthRemainder_spec (p : ) [hp : Fact ()] {k : Type u_1} [] [CharP k p] (n : ) (x : ) (y : ) :
(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) + WittVector.nthRemainder p n (WittVector.truncateFun (n + 1) x) (WittVector.truncateFun (n + 1) y)