Documentation

Mathlib.RingTheory.WittVector.StructurePolynomial

Witt structure polynomials #

In this file we prove the main theorem that makes the whole theory of Witt vectors work. Briefly, consider a polynomial Φ : MvPolynomial idx ℤ over the integers, with polynomials variables indexed by an arbitrary type idx.

Then there exists a unique family of polynomials φ : ℕ → MvPolynomial (idx × ℕ) Φ such that for all n : ℕ we have (wittStructureInt_existsUnique)

bind₁ φ (wittPolynomial p ℤ n) = bind₁ (fun i ↦ (rename (prod.mk i) (wittPolynomial p ℤ n))) Φ

In other words: evaluating the n-th Witt polynomial on the family φ is the same as evaluating Φ on the (appropriately renamed) n-th Witt polynomials.

N.b.: As far as we know, these polynomials do not have a name in the literature, so we have decided to call them the “Witt structure polynomials”. See wittStructureInt.

Special cases #

With the main result of this file in place, we apply it to certain special polynomials. For example, by taking Φ = X tt + X ff resp. Φ = X tt * X ff we obtain families of polynomials witt_add resp. witt_mul (with type ℕ → MvPolynomial (Bool × ℕ) ℤ) that will be used in later files to define the addition and multiplication on the ring of Witt vectors.

Outline of the proof #

The proof of wittStructureInt_existsUnique is rather technical, and takes up most of this file.

We start by proving the analogous version for polynomials with rational coefficients, instead of integer coefficients. In this case, the solution is rather easy, since the Witt polynomials form a faithful change of coordinates in the polynomial ring MvPolynomial ℕ ℚ. We therefore obtain a family of polynomials wittStructureRat Φ for every Φ : MvPolynomial idx ℚ.

If Φ has integer coefficients, then the polynomials wittStructureRat Φ n do so as well. Proving this claim is the essential core of this file, and culminates in map_wittStructureInt, which proves that upon mapping the coefficients of wittStructureInt Φ n from the integers to the rationals, one obtains wittStructureRat Φ n. Ultimately, the proof of map_wittStructureInt relies on

dvd_sub_pow_of_dvd_sub {R : Type*} [CommRing R] {p : ℕ} {a b : R} :
    (p : R) ∣ a - b → ∀ (k : ℕ), (p : R) ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k

Main results #

References #

wittPolynomial p R n is the n-th Witt polynomial with respect to a prime p with coefficients in a commutative ring R. It is defined as:

∑_{i ≤ n} p^i X_i^{p^{n-i}} ∈ R[X_0, X_1, X_2, …].

Equations
Instances For

    wittPolynomial p R n is the n-th Witt polynomial with respect to a prime p with coefficients in a commutative ring R. It is defined as:

    ∑_{i ≤ n} p^i X_i^{p^{n-i}} ∈ R[X_0, X_1, X_2, …].

    Equations
    Instances For
      noncomputable def wittStructureRat (p : ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ) (n : ) :

      wittStructureRat Φ is a family of polynomials ℕ → MvPolynomial (idx × ℕ) ℚ that are uniquely characterised by the property that

      bind₁ (wittStructureRat p Φ) (wittPolynomial p ℚ n) =
      bind₁ (fun i ↦ (rename (prod.mk i) (wittPolynomial p ℚ n))) Φ
      

      In other words: evaluating the n-th Witt polynomial on the family wittStructureRat Φ is the same as evaluating Φ on the (appropriately renamed) n-th Witt polynomials.

      See wittStructureRat_prop for this property, and wittStructureRat_existsUnique for the fact that wittStructureRat gives the unique family of polynomials with this property.

      These polynomials turn out to have integral coefficients, but it requires some effort to show this. See wittStructureInt for the version with integral coefficients, and map_wittStructureInt for the fact that it is equal to wittStructureRat when mapped to polynomials over the rationals.

      Equations
      Instances For
        theorem wittStructureRat_existsUnique (p : ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ) :
        ∃! φ : MvPolynomial (idx × ) , ∀ (n : ), (MvPolynomial.bind₁ φ) (wittPolynomial p n) = (MvPolynomial.bind₁ fun (i : idx) => (MvPolynomial.rename (Prod.mk i)) (wittPolynomial p n)) Φ
        theorem wittStructureRat_rec_aux (p : ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ) (n : ) :
        wittStructureRat p Φ n * MvPolynomial.C (p ^ n) = (MvPolynomial.bind₁ fun (b : idx) => (MvPolynomial.rename fun (i : ) => (b, i)) (wittPolynomial p n)) Φ - iFinset.range n, MvPolynomial.C (p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
        theorem wittStructureRat_rec (p : ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ) (n : ) :
        wittStructureRat p Φ n = MvPolynomial.C (1 / p ^ n) * ((MvPolynomial.bind₁ fun (b : idx) => (MvPolynomial.rename fun (i : ) => (b, i)) (wittPolynomial p n)) Φ - iFinset.range n, MvPolynomial.C (p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i))

        Write wittStructureRat p φ n in terms of wittStructureRat p φ i for i < n.

        noncomputable def wittStructureInt (p : ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ) (n : ) :

        wittStructureInt Φ is a family of polynomials ℕ → MvPolynomial (idx × ℕ) ℤ that are uniquely characterised by the property that

        bind₁ (wittStructureInt p Φ) (wittPolynomial p ℤ n) =
        bind₁ (fun i ↦ (rename (prod.mk i) (wittPolynomial p ℤ n))) Φ
        

        In other words: evaluating the n-th Witt polynomial on the family wittStructureInt Φ is the same as evaluating Φ on the (appropriately renamed) n-th Witt polynomials.

        See wittStructureInt_prop for this property, and wittStructureInt_existsUnique for the fact that wittStructureInt gives the unique family of polynomials with this property.

        Equations
        Instances For
          theorem C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum {p : } {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ) (n : ) (IH : m < n, (MvPolynomial.map (Int.castRingHom )) (wittStructureInt p Φ m) = wittStructureRat p ((MvPolynomial.map (Int.castRingHom )) Φ) m) :
          MvPolynomial.C (p ^ n) (MvPolynomial.bind₁ fun (b : idx) => (MvPolynomial.rename fun (i : ) => (b, i)) (wittPolynomial p n)) Φ - iFinset.range n, MvPolynomial.C (p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)
          theorem eq_wittStructureInt (p : ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ) (φ : MvPolynomial (idx × ) ) (h : ∀ (n : ), (MvPolynomial.bind₁ φ) (wittPolynomial p n) = (MvPolynomial.bind₁ fun (i : idx) => (MvPolynomial.rename (Prod.mk i)) (wittPolynomial p n)) Φ) :
          theorem wittStructureInt_existsUnique (p : ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ) :
          ∃! φ : MvPolynomial (idx × ) , ∀ (n : ), (MvPolynomial.bind₁ φ) (wittPolynomial p n) = (MvPolynomial.bind₁ fun (i : idx) => (MvPolynomial.rename (Prod.mk i)) (wittPolynomial p n)) Φ
          theorem witt_structure_prop (p : ) {R : Type u_1} {idx : Type u_2} [CommRing R] [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ) (n : ) :
          theorem wittStructureInt_rename (p : ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] {σ : Type u_3} (Φ : MvPolynomial idx ) (f : idxσ) (n : ) :
          @[simp]
          theorem constantCoeff_wittStructureRat_zero (p : ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ) :
          MvPolynomial.constantCoeff (wittStructureRat p Φ 0) = MvPolynomial.constantCoeff Φ
          theorem constantCoeff_wittStructureRat (p : ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ) (h : MvPolynomial.constantCoeff Φ = 0) (n : ) :
          MvPolynomial.constantCoeff (wittStructureRat p Φ n) = 0
          @[simp]
          theorem constantCoeff_wittStructureInt_zero (p : ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ) :
          MvPolynomial.constantCoeff (wittStructureInt p Φ 0) = MvPolynomial.constantCoeff Φ
          theorem constantCoeff_wittStructureInt (p : ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ) (h : MvPolynomial.constantCoeff Φ = 0) (n : ) :
          MvPolynomial.constantCoeff (wittStructureInt p Φ n) = 0
          theorem wittStructureRat_vars (p : ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] [Fintype idx] (Φ : MvPolynomial idx ) (n : ) :
          (wittStructureRat p Φ n).vars Finset.univ ×ˢ Finset.range (n + 1)
          theorem wittStructureInt_vars (p : ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] [Fintype idx] (Φ : MvPolynomial idx ) (n : ) :
          (wittStructureInt p Φ n).vars Finset.univ ×ˢ Finset.range (n + 1)