Documentation

Mathlib.RingTheory.WittVector.Defs

Witt vectors #

In this file we define the type of p-typical Witt vectors and ring operations on it. The ring axioms are verified in RingTheory.WittVector.Basic.

For a fixed commutative ring R and prime p, a Witt vector x : π•Ž R is an infinite sequence β„• β†’ R of elements of R. However, the ring operations + and * are not defined in the obvious component-wise way. Instead, these operations are defined via certain polynomials using the machinery in StructurePolynomial.lean. The nth value of the sum of two Witt vectors can depend on the 0-th through nth values of the summands. This effectively simulates a β€œcarrying” operation.

Main definitions #

Notation #

We use notation π•Ž R, entered \bbW, for the Witt vectors over R.

References #

structure WittVector (p : β„•) (R : Type u_1) :
Type u_1
  • mk' :: (
    • coeff : β„• β†’ R

      x.coeff n is the nth coefficient of the Witt vector x.

      This concept does not have a standard name in the literature.

  • )

witt_vector p R is the ring of p-typical Witt vectors over the commutative ring R, where p is a prime number.

If p is invertible in R, this ring is isomorphic to β„• β†’ R (the product of β„• copies of R). If R is a ring of characteristic p, then witt_vector p R is a ring of characteristic 0. The canonical example is witt_vector p (zmod p), which is isomorphic to the p-adic integers β„€_[p].

Instances For
    def WittVector.mk (p : β„•) {R : Type u_1} (coeff : β„• β†’ R) :

    Construct a Witt vector mk p x : π•Ž R from a sequence x of elements of R.

    Instances For
      theorem WittVector.ext {p : β„•} {R : Type u_1} {x : WittVector p R} {y : WittVector p R} (h : βˆ€ (n : β„•), WittVector.coeff x n = WittVector.coeff y n) :
      x = y
      theorem WittVector.ext_iff {p : β„•} {R : Type u_1} {x : WittVector p R} {y : WittVector p R} :
      x = y ↔ βˆ€ (n : β„•), WittVector.coeff x n = WittVector.coeff y n
      theorem WittVector.coeff_mk (p : β„•) {R : Type u_1} (x : β„• β†’ R) :
      (WittVector.mk p x).coeff = x

      The polynomials used for defining the element 0 of the ring of Witt vectors.

      Instances For

        The polynomials used for defining the element 1 of the ring of Witt vectors.

        Instances For

          The polynomials used for defining the addition of the ring of Witt vectors.

          Instances For

            The polynomials used for defining repeated addition of the ring of Witt vectors.

            Instances For

              The polynomials used for defining repeated addition of the ring of Witt vectors.

              Instances For

                The polynomials used for describing the subtraction of the ring of Witt vectors.

                Instances For

                  The polynomials used for defining the multiplication of the ring of Witt vectors.

                  Instances For

                    The polynomials used for defining the negation of the ring of Witt vectors.

                    Instances For

                      The polynomials used for defining repeated addition of the ring of Witt vectors.

                      Instances For
                        def WittVector.peval {R : Type u_1} [CommRing R] {k : β„•} (Ο† : MvPolynomial (Fin k Γ— β„•) β„€) (x : Fin k β†’ β„• β†’ R) :
                        R

                        An auxiliary definition used in witt_vector.eval. Evaluates a polynomial whose variables come from the disjoint union of k copies of β„•, with a curried evaluation x. This can be defined more generally but we use only a specific instance here.

                        Instances For
                          def WittVector.eval {p : β„•} {R : Type u_1} [CommRing R] {k : β„•} (Ο† : β„• β†’ MvPolynomial (Fin k Γ— β„•) β„€) (x : Fin k β†’ WittVector p R) :

                          Let Ο† be a family of polynomials, indexed by natural numbers, whose variables come from the disjoint union of k copies of β„•, and let xα΅’ be a Witt vector for 0 ≀ i < k.

                          eval Ο† x evaluates Ο† mapping the variable X_(i, n) to the nth coefficient of xα΅’.

                          Instantiating Ο† with certain polynomials defined in structure_polynomial.lean establishes the ring operations on π•Ž R. For example, witt_vector.witt_add is such a Ο† with k = 2; evaluating this at (xβ‚€, x₁) gives us the sum of two Witt vectors xβ‚€ + x₁.

                          Instances For
                            @[simp]
                            @[simp]
                            theorem WittVector.wittOne_pos_eq_zero (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) (hn : 0 < n) :
                            @[simp]
                            theorem WittVector.constantCoeff_wittAdd (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                            ↑MvPolynomial.constantCoeff (WittVector.wittAdd p n) = 0
                            @[simp]
                            theorem WittVector.constantCoeff_wittSub (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                            ↑MvPolynomial.constantCoeff (WittVector.wittSub p n) = 0
                            @[simp]
                            theorem WittVector.constantCoeff_wittMul (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                            ↑MvPolynomial.constantCoeff (WittVector.wittMul p n) = 0
                            @[simp]
                            theorem WittVector.constantCoeff_wittNeg (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                            ↑MvPolynomial.constantCoeff (WittVector.wittNeg p n) = 0
                            @[simp]
                            theorem WittVector.constantCoeff_wittNSMul (p : β„•) [hp : Fact (Nat.Prime p)] (m : β„•) (n : β„•) :
                            ↑MvPolynomial.constantCoeff (WittVector.wittNSMul p m n) = 0
                            @[simp]
                            theorem WittVector.constantCoeff_wittZSMul (p : β„•) [hp : Fact (Nat.Prime p)] (z : β„€) (n : β„•) :
                            ↑MvPolynomial.constantCoeff (WittVector.wittZSMul p z n) = 0
                            @[simp]
                            theorem WittVector.zero_coeff (p : β„•) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] (n : β„•) :
                            @[simp]
                            theorem WittVector.one_coeff_zero (p : β„•) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] :
                            @[simp]
                            theorem WittVector.one_coeff_eq_of_pos (p : β„•) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] (n : β„•) (hn : 0 < n) :
                            @[simp]
                            theorem WittVector.v2_coeff {p' : β„•} {R' : Type u_2} (x : WittVector p' R') (y : WittVector p' R') (i : Fin 2) :
                            (Matrix.vecCons x ![y] i).coeff = Matrix.vecCons x.coeff ![y.coeff] i
                            theorem WittVector.add_coeff {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x : WittVector p R) (y : WittVector p R) (n : β„•) :
                            WittVector.coeff (x + y) n = WittVector.peval (WittVector.wittAdd p n) ![x.coeff, y.coeff]
                            theorem WittVector.sub_coeff {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x : WittVector p R) (y : WittVector p R) (n : β„•) :
                            WittVector.coeff (x - y) n = WittVector.peval (WittVector.wittSub p n) ![x.coeff, y.coeff]
                            theorem WittVector.mul_coeff {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x : WittVector p R) (y : WittVector p R) (n : β„•) :
                            WittVector.coeff (x * y) n = WittVector.peval (WittVector.wittMul p n) ![x.coeff, y.coeff]
                            theorem WittVector.neg_coeff {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x : WittVector p R) (n : β„•) :
                            theorem WittVector.nsmul_coeff {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (m : β„•) (x : WittVector p R) (n : β„•) :
                            theorem WittVector.zsmul_coeff {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (m : β„€) (x : WittVector p R) (n : β„•) :
                            theorem WittVector.pow_coeff {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (m : β„•) (x : WittVector p R) (n : β„•) :
                            theorem WittVector.add_coeff_zero {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x : WittVector p R) (y : WittVector p R) :
                            theorem WittVector.mul_coeff_zero {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x : WittVector p R) (y : WittVector p R) :