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 #

(∑ 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 (Nat.Prime p)] (n : ) :
    (WittVector.wittPolyProd p n).vars Finset.univ ×ˢ Finset.range (n + 1)

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

    Equations
    Instances For

      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 (Nat.Prime p)] (n : ) :
        (WittVector.remainder p n).vars Finset.univ ×ˢ Finset.range (n + 1)

        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 (Nat.Prime p)] (n : ) :
          iFinset.range (n + 1), p ^ i * WittVector.wittMul p i ^ p ^ (n - i) = WittVector.wittPolyProd 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) * (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)) + WittVector.remainder p n
          theorem WittVector.mul_polyOfInterest_aux4 (p : ) [hp : Fact (Nat.Prime p)] (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) * (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)) + (WittVector.remainder p n - WittVector.wittPolyProdRemainder p (n + 1))
          theorem WittVector.mul_polyOfInterest_vars (p : ) [hp : Fact (Nat.Prime p)] (n : ) :
          (p ^ (n + 1) * WittVector.polyOfInterest p n).vars Finset.univ ×ˢ Finset.range (n + 1)
          theorem WittVector.polyOfInterest_vars_eq (p : ) [hp : Fact (Nat.Prime p)] (n : ) :
          (WittVector.polyOfInterest p 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) * (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 : ) :
          (WittVector.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 : WittVector p k) (y : WittVector p k) :
          WittVector.peval (WittVector.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) * 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 (Nat.Prime p)] {k : Type u_1} [CommRing k] [CharP k p] (n : ) (x : WittVector p k) (y : WittVector p k) :
          WittVector.peval (WittVector.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) kTruncatedWittVector p (n + 1) kk), ∀ (x y : WittVector p k), 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 (Nat.Prime p)] (k : Type u_1) [CommRing k] [CharP k p] (n : ) :
          ∃ (f : TruncatedWittVector p (n + 1) kTruncatedWittVector p (n + 1) kk), ∀ (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 (WittVector.truncateFun (n + 1) x) (WittVector.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
          Instances For
            theorem WittVector.nthRemainder_spec (p : ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] [CharP k p] (n : ) (x : WittVector p k) (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) + WittVector.nthRemainder p n (WittVector.truncateFun (n + 1) x) (WittVector.truncateFun (n + 1) y)