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 Mathlib/RingTheory/WittVector/Basic.lean.

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 Mathlib/RingTheory/WittVector/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

WittVector 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 WittVector p R is a ring of characteristic 0. The canonical example is WittVector p (ZMod p), which is isomorphic to the p-adic integers β„€_[p].

  • 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.

  • )
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.

    Equations
    Instances For
      theorem WittVector.ext {p : β„•} {R : Type u_1} {x : WittVector p R} {y : WittVector p R} (h : βˆ€ (n : β„•), x.coeff n = y.coeff n) :
      x = y
      theorem WittVector.ext_iff {p : β„•} {R : Type u_1} {x : WittVector p R} {y : WittVector p R} :
      x = y ↔ βˆ€ (n : β„•), x.coeff n = y.coeff n
      theorem WittVector.coeff_mk (p : β„•) {R : Type u_1} (x : β„• β†’ R) :
      (WittVector.mk p x).coeff = x
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • β‹― = β‹―

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

      Equations
      Instances For

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

        Equations
        Instances For

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

          Equations
          Instances For

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

            Equations
            Instances For

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

              Equations
              Instances For

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

                Equations
                Instances For

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

                  Equations
                  Instances For

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

                    Equations
                    Instances For

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

                      Equations
                      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 WittVector.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.

                        Equations
                        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 Mathlib/RingTheory/WittVector/StructurePolynomial.lean establishes the ring operations on π•Ž R. For example, WittVector.wittAdd is such a Ο† with k = 2; evaluating this at (xβ‚€, x₁) gives us the sum of two Witt vectors xβ‚€ + x₁.

                          Equations
                          Instances For
                            instance WittVector.instZero {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            Equations
                            Equations
                            instance WittVector.instOne {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            Equations
                            instance WittVector.instAdd {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            Equations
                            instance WittVector.instSub {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            Equations
                            instance WittVector.hasNatScalar {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            Equations
                            instance WittVector.hasIntScalar {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            Equations
                            instance WittVector.instMul {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            Equations
                            instance WittVector.instNeg {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            Equations
                            instance WittVector.hasNatPow {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            Equations
                            instance WittVector.instNatCast {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            Equations
                            instance WittVector.instIntCast {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            Equations
                            @[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) :
                            (![x, y] i).coeff = ![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 : β„•) :
                            (x + y).coeff 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 : β„•) :
                            (x - y).coeff 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 : β„•) :
                            (x * y).coeff 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 : β„•) :
                            (-x).coeff n = WittVector.peval (WittVector.wittNeg p n) ![x.coeff]
                            theorem WittVector.nsmul_coeff {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (m : β„•) (x : WittVector p R) (n : β„•) :
                            (m β€’ x).coeff n = WittVector.peval (WittVector.wittNSMul p m n) ![x.coeff]
                            theorem WittVector.zsmul_coeff {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (m : β„€) (x : WittVector p R) (n : β„•) :
                            (m β€’ x).coeff n = WittVector.peval (WittVector.wittZSMul p m n) ![x.coeff]
                            theorem WittVector.pow_coeff {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (m : β„•) (x : WittVector p R) (n : β„•) :
                            (x ^ m).coeff n = WittVector.peval (WittVector.wittPow p m n) ![x.coeff]
                            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) :
                            (x + y).coeff 0 = x.coeff 0 + y.coeff 0
                            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) :
                            (x * y).coeff 0 = x.coeff 0 * y.coeff 0
                            theorem WittVector.wittAdd_vars (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                            (WittVector.wittAdd p n).vars βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)
                            theorem WittVector.wittSub_vars (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                            (WittVector.wittSub p n).vars βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)
                            theorem WittVector.wittMul_vars (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                            (WittVector.wittMul p n).vars βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)
                            theorem WittVector.wittNeg_vars (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                            (WittVector.wittNeg p n).vars βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)
                            theorem WittVector.wittNSMul_vars (p : β„•) [hp : Fact (Nat.Prime p)] (m : β„•) (n : β„•) :
                            (WittVector.wittNSMul p m n).vars βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)
                            theorem WittVector.wittZSMul_vars (p : β„•) [hp : Fact (Nat.Prime p)] (m : β„€) (n : β„•) :
                            (WittVector.wittZSMul p m n).vars βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)
                            theorem WittVector.wittPow_vars (p : β„•) [hp : Fact (Nat.Prime p)] (m : β„•) (n : β„•) :
                            (WittVector.wittPow p m n).vars βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)