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.

def WittVector.wittPolyProd (p n : ℕ) : MvPolynomial (Fin 2 × ℕ) ℤ

(∑ 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

• WittVector.wittPolyProd p n = (MvPolynomial.rename (Prod.mk 0)) (wittPolynomial p ℤ n) * (MvPolynomial.rename (Prod.mk 1)) (wittPolynomial p ℤ n)

theorem WittVector.wittPolyProd_vars (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : (wittPolyProd p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)

def WittVector.wittPolyProdRemainder (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : MvPolynomial (Fin 2 × ℕ) ℤ

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

Equations

• WittVector.wittPolyProdRemainder p n = ∑ i ∈ Finset.range n, ↑p ^ i * WittVector.wittMul p i ^ p ^ (n - i)

theorem WittVector.wittPolyProdRemainder_vars (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : (wittPolyProdRemainder p n).vars ⊆ Finset.univ ×ˢ Finset.range n

def WittVector.remainder (p n : ℕ) : MvPolynomial (Fin 2 × ℕ) ℤ

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.

theorem WittVector.remainder_vars (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : (remainder p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)

def WittVector.polyOfInterest (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : MvPolynomial (Fin 2 × ℕ) ℤ

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.

theorem WittVector.mul_polyOfInterest_aux1 (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : ∑ i ∈ Finset.range (n + 1), ↑p ^ i * wittMul p i ^ p ^ (n - i) = wittPolyProd p n

theorem WittVector.mul_polyOfInterest_aux2 (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : ↑p ^ n * wittMul p n + wittPolyProdRemainder p n = wittPolyProd p n

theorem WittVector.mul_polyOfInterest_aux3 (p n : ℕ) : 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) * (MvPolynomial.rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) + ↑p ^ (n + 1) * MvPolynomial.X (1, n + 1) * (MvPolynomial.rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) + remainder p n

theorem WittVector.mul_polyOfInterest_aux4 (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : ↑p ^ (n + 1) * 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) * (MvPolynomial.rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) + ↑p ^ (n + 1) * MvPolynomial.X (1, n + 1) * (MvPolynomial.rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) + (remainder p n - wittPolyProdRemainder p (n + 1))

theorem WittVector.mul_polyOfInterest_aux5 (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : ↑p ^ (n + 1) * polyOfInterest p n = remainder p n - wittPolyProdRemainder p (n + 1)

theorem WittVector.mul_polyOfInterest_vars (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : (↑p ^ (n + 1) * polyOfInterest p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)

theorem WittVector.polyOfInterest_vars_eq (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : (polyOfInterest p n).vars = (↑p ^ (n + 1) * (wittMul p (n + 1) + ↑p ^ (n + 1) * MvPolynomial.X (0, n + 1) * MvPolynomial.X (1, n + 1) - MvPolynomial.X (0, n + 1) * (MvPolynomial.rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) - MvPolynomial.X (1, n + 1) * (MvPolynomial.rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars

theorem WittVector.polyOfInterest_vars (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : (polyOfInterest p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)

theorem WittVector.peval_polyOfInterest (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] (n : ℕ) (x y : WittVector p k) : peval (polyOfInterest p n) ![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) * ∑ i ∈ Finset.range (n + 1 + 1), ↑p ^ i * x.coeff i ^ p ^ (n + 1 - i) - x.coeff (n + 1) * ∑ i ∈ Finset.range (n + 1 + 1), ↑p ^ i * y.coeff i ^ p ^ (n + 1 - i)

theorem WittVector.peval_polyOfInterest' (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] [CharP k p] (n : ℕ) (x y : WittVector p k) : peval (polyOfInterest p n) ![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 (Nat.Prime p)] (k : Type u_1) [CommRing k] [CharP k p] (n : ℕ) : ∃ (f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k), ∀ (x y : WittVector p k), f (truncateFun (n + 1) x) (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 (Nat.Prime p)] (k : Type u_1) [CommRing k] [CharP k p] (n : ℕ) : ∃ (f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k), ∀ (x y : WittVector 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 (truncateFun (n + 1) x) (truncateFun (n + 1) y)

def WittVector.nthRemainder (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] [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

• WittVector.nthRemainder p n = Classical.choose ⋯

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