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 #

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 : ℕ) :

mv_polynomial (fin 2 × ℕ) ℤ

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

witt_vector.witt_poly_prod p n = ⇑(mv_polynomial.rename (prod.mk 0)) (witt_polynomial p ℤ n) * ⇑(mv_polynomial.rename (prod.mk 1)) (witt_polynomial p ℤ n)

theorem witt_vector.witt_poly_prod_vars (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :

(witt_vector.witt_poly_prod p n).vars ⊆ finset.univ ×ˢ finset.range (n + 1)

noncomputable def witt_vector.witt_poly_prod_remainder (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :

mv_polynomial (fin 2 × ℕ) ℤ

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

Equations

witt_vector.witt_poly_prod_remainder p n = (finset.range n).sum (λ (i : ℕ), ↑p ^ i * witt_vector.witt_mul p i ^ p ^ (n - i))

theorem witt_vector.witt_poly_prod_remainder_vars (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :

(witt_vector.witt_poly_prod_remainder p n).vars ⊆ finset.univ ×ˢ finset.range n

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

mv_polynomial (fin 2 × ℕ) ℤ

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

witt_vector.remainder p n = (finset.range (n + 1)).sum (λ (x : ℕ), ⇑(mv_polynomial.rename (prod.mk 0)) (⇑(mv_polynomial.monomial (finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) * (finset.range (n + 1)).sum (λ (x : ℕ), ⇑(mv_polynomial.rename (prod.mk 1)) (⇑(mv_polynomial.monomial (finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)))

theorem witt_vector.remainder_vars (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :

(witt_vector.remainder p n).vars ⊆ finset.univ ×ˢ finset.range (n + 1)

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

mv_polynomial (fin 2 × ℕ) ℤ

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

Equations

witt_vector.poly_of_interest p n = witt_vector.witt_mul p (n + 1) + ↑p ^ (n + 1) * mv_polynomial.X (0, n + 1) * mv_polynomial.X (1, n + 1) - mv_polynomial.X (0, n + 1) * ⇑(mv_polynomial.rename (prod.mk 1)) (witt_polynomial p ℤ (n + 1)) - mv_polynomial.X (1, n + 1) * ⇑(mv_polynomial.rename (prod.mk 0)) (witt_polynomial p ℤ (n + 1))

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.mul_poly_of_interest_aux2 (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :

↑p ^ n * witt_vector.witt_mul p n + witt_vector.witt_poly_prod_remainder p n = witt_vector.witt_poly_prod p n

theorem witt_vector.mul_poly_of_interest_aux3 (p n : ℕ) :

witt_vector.witt_poly_prod p (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) * ⇑(mv_polynomial.rename (prod.mk 1)) (witt_polynomial p ℤ (n + 1)) + ↑p ^ (n + 1) * mv_polynomial.X (1, n + 1) * ⇑(mv_polynomial.rename (prod.mk 0)) (witt_polynomial p ℤ (n + 1)) + witt_vector.remainder p n

theorem witt_vector.mul_poly_of_interest_aux4 (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :

↑p ^ (n + 1) * witt_vector.witt_mul p (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) * ⇑(mv_polynomial.rename (prod.mk 1)) (witt_polynomial p ℤ (n + 1)) + ↑p ^ (n + 1) * mv_polynomial.X (1, n + 1) * ⇑(mv_polynomial.rename (prod.mk 0)) (witt_polynomial p ℤ (n + 1)) + (witt_vector.remainder p n - witt_vector.witt_poly_prod_remainder p (n + 1))

theorem witt_vector.mul_poly_of_interest_aux5 (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :

↑p ^ (n + 1) * witt_vector.poly_of_interest p n = witt_vector.remainder p n - witt_vector.witt_poly_prod_remainder p (n + 1)

theorem witt_vector.mul_poly_of_interest_vars (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :

(↑p ^ (n + 1) * witt_vector.poly_of_interest p n).vars ⊆ finset.univ ×ˢ finset.range (n + 1)

theorem witt_vector.poly_of_interest_vars_eq (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :

(witt_vector.poly_of_interest p n).vars = (↑p ^ (n + 1) * (witt_vector.witt_mul p (n + 1) + ↑p ^ (n + 1) * mv_polynomial.X (0, n + 1) * mv_polynomial.X (1, n + 1) - mv_polynomial.X (0, n + 1) * ⇑(mv_polynomial.rename (prod.mk 1)) (witt_polynomial p ℤ (n + 1)) - mv_polynomial.X (1, n + 1) * ⇑(mv_polynomial.rename (prod.mk 0)) (witt_polynomial p ℤ (n + 1)))).vars

theorem witt_vector.poly_of_interest_vars (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :

(witt_vector.poly_of_interest p n).vars ⊆ finset.univ ×ˢ finset.range (n + 1)

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

witt_vector.nth_remainder p n = classical.some _

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)