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 #

source
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
    source
    def WittVector.mk (p : β„•) {R : Type u_1} (coeff : β„• β†’ R) :
    WittVector p R

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

    This is preferred over WittVector.mk' because it has p explicit.

    Equations
      Instances For
        source
        theorem WittVector.ext {p : β„•} {R : Type u_1} {x y : WittVector p R} (h : βˆ€ (n : β„•), x.coeff n = y.coeff n) :
        x = y
        source
        theorem WittVector.ext_iff {p : β„•} {R : Type u_1} {x y : WittVector p R} :
        x = y ↔ βˆ€ (n : β„•), x.coeff n = y.coeff n
        source
        @[simp]
        theorem WittVector.coeff_mk (p : β„•) {R : Type u_1} (x : β„• β†’ R) :
        (mk p x).coeff = x
        source
        instance WittVector.instFunctor (p : β„•) :
        Functor (WittVector p)
        Equations
          source
          instance WittVector.instLawfulFunctor (p : β„•) :
          LawfulFunctor (WittVector p)
          source
          def WittVector.wittZero (p : β„•) [hp : Fact (Nat.Prime p)] :
          β„• β†’ MvPolynomial (Fin 0 Γ— β„•) β„€

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

          Equations
            Instances For
              source
              def WittVector.wittOne (p : β„•) [hp : Fact (Nat.Prime p)] :
              β„• β†’ MvPolynomial (Fin 0 Γ— β„•) β„€

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

              Equations
                Instances For
                  source
                  def WittVector.wittAdd (p : β„•) [hp : Fact (Nat.Prime p)] :
                  β„• β†’ MvPolynomial (Fin 2 Γ— β„•) β„€

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

                  Equations
                    Instances For
                      source
                      def WittVector.wittNSMul (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                      β„• β†’ MvPolynomial (Fin 1 Γ— β„•) β„€

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

                      Equations
                        Instances For
                          source
                          def WittVector.wittZSMul (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„€) :
                          β„• β†’ MvPolynomial (Fin 1 Γ— β„•) β„€

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

                          Equations
                            Instances For
                              source
                              def WittVector.wittSub (p : β„•) [hp : Fact (Nat.Prime p)] :
                              β„• β†’ MvPolynomial (Fin 2 Γ— β„•) β„€

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

                              Equations
                                Instances For
                                  source
                                  def WittVector.wittMul (p : β„•) [hp : Fact (Nat.Prime p)] :
                                  β„• β†’ MvPolynomial (Fin 2 Γ— β„•) β„€

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

                                  Equations
                                    Instances For
                                      source
                                      def WittVector.wittNeg (p : β„•) [hp : Fact (Nat.Prime p)] :
                                      β„• β†’ MvPolynomial (Fin 1 Γ— β„•) β„€

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

                                      Equations
                                        Instances For
                                          source
                                          def WittVector.wittPow (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                                          β„• β†’ MvPolynomial (Fin 1 Γ— β„•) β„€

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

                                          Equations
                                            Instances For
                                              source
                                              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
                                                  source
                                                  def WittVector.eval {p : β„•} {R : Type u_1} [CommRing R] {k : β„•} (Ο† : β„• β†’ MvPolynomial (Fin k Γ— β„•) β„€) (x : Fin k β†’ WittVector p R) :
                                                  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
                                                      source
                                                      instance WittVector.instZero {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                                                      Zero (WittVector p R)
                                                      Equations
                                                        source
                                                        instance WittVector.instInhabited {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                                                        Inhabited (WittVector p R)
                                                        Equations
                                                          source
                                                          instance WittVector.instOne {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                                                          One (WittVector p R)
                                                          Equations
                                                            source
                                                            instance WittVector.instAdd {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                                                            Add (WittVector p R)
                                                            Equations
                                                              source
                                                              instance WittVector.instSub {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                                                              Sub (WittVector p R)
                                                              Equations
                                                                source
                                                                instance WittVector.hasNatScalar {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                                                                SMul β„• (WittVector p R)
                                                                Equations
                                                                  source
                                                                  instance WittVector.hasIntScalar {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                                                                  SMul β„€ (WittVector p R)
                                                                  Equations
                                                                    source
                                                                    instance WittVector.instMul {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                                                                    Mul (WittVector p R)
                                                                    Equations
                                                                      source
                                                                      instance WittVector.instNeg {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                                                                      Neg (WittVector p R)
                                                                      Equations
                                                                        source
                                                                        instance WittVector.hasNatPow {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                                                                        Pow (WittVector p R) β„•
                                                                        Equations
                                                                          source
                                                                          instance WittVector.instNatCast {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                                                                          NatCast (WittVector p R)
                                                                          Equations
                                                                            source
                                                                            instance WittVector.instIntCast {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                                                                            IntCast (WittVector p R)
                                                                            Equations
                                                                              source
                                                                              @[simp]
                                                                              theorem WittVector.wittZero_eq_zero (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                                                                              wittZero p n = 0
                                                                              source
                                                                              @[simp]
                                                                              theorem WittVector.wittOne_zero_eq_one (p : β„•) [hp : Fact (Nat.Prime p)] :
                                                                              wittOne p 0 = 1
                                                                              source
                                                                              @[simp]
                                                                              theorem WittVector.wittOne_pos_eq_zero (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) (hn : 0 < n) :
                                                                              wittOne p n = 0
                                                                              source
                                                                              @[simp]
                                                                              theorem WittVector.wittAdd_zero (p : β„•) [hp : Fact (Nat.Prime p)] :
                                                                              wittAdd p 0 = MvPolynomial.X (0, 0) + MvPolynomial.X (1, 0)
                                                                              source
                                                                              @[simp]
                                                                              theorem WittVector.wittSub_zero (p : β„•) [hp : Fact (Nat.Prime p)] :
                                                                              wittSub p 0 = MvPolynomial.X (0, 0) - MvPolynomial.X (1, 0)
                                                                              source
                                                                              @[simp]
                                                                              theorem WittVector.wittMul_zero (p : β„•) [hp : Fact (Nat.Prime p)] :
                                                                              wittMul p 0 = MvPolynomial.X (0, 0) * MvPolynomial.X (1, 0)
                                                                              source
                                                                              @[simp]
                                                                              theorem WittVector.wittNeg_zero (p : β„•) [hp : Fact (Nat.Prime p)] :
                                                                              wittNeg p 0 = -MvPolynomial.X (0, 0)
                                                                              source
                                                                              @[simp]
                                                                              theorem WittVector.constantCoeff_wittAdd (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                                                                              MvPolynomial.constantCoeff (wittAdd p n) = 0
                                                                              source
                                                                              @[simp]
                                                                              theorem WittVector.constantCoeff_wittSub (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                                                                              MvPolynomial.constantCoeff (wittSub p n) = 0
                                                                              source
                                                                              @[simp]
                                                                              theorem WittVector.constantCoeff_wittMul (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                                                                              MvPolynomial.constantCoeff (wittMul p n) = 0
                                                                              source
                                                                              @[simp]
                                                                              theorem WittVector.constantCoeff_wittNeg (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                                                                              MvPolynomial.constantCoeff (wittNeg p n) = 0
                                                                              source
                                                                              @[simp]
                                                                              theorem WittVector.constantCoeff_wittNSMul (p : β„•) [hp : Fact (Nat.Prime p)] (m n : β„•) :
                                                                              MvPolynomial.constantCoeff (wittNSMul p m n) = 0
                                                                              source
                                                                              @[simp]
                                                                              theorem WittVector.constantCoeff_wittZSMul (p : β„•) [hp : Fact (Nat.Prime p)] (z : β„€) (n : β„•) :
                                                                              MvPolynomial.constantCoeff (wittZSMul p z n) = 0
                                                                              source
                                                                              @[simp]
                                                                              theorem WittVector.zero_coeff (p : β„•) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] (n : β„•) :
                                                                              coeff 0 n = 0
                                                                              source
                                                                              @[simp]
                                                                              theorem WittVector.one_coeff_zero (p : β„•) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] :
                                                                              coeff 1 0 = 1
                                                                              source
                                                                              @[simp]
                                                                              theorem WittVector.one_coeff_eq_of_pos (p : β„•) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] (n : β„•) (hn : 0 < n) :
                                                                              coeff 1 n = 0
                                                                              source
                                                                              @[simp]
                                                                              theorem WittVector.v2_coeff {p' : β„•} {R' : Type u_2} (x y : WittVector p' R') (i : Fin 2) :
                                                                              (![x, y] i).coeff = ![x.coeff, y.coeff] i
                                                                              source
                                                                              theorem WittVector.add_coeff {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x y : WittVector p R) (n : β„•) :
                                                                              (x + y).coeff n = peval (wittAdd p n) ![x.coeff, y.coeff]
                                                                              source
                                                                              theorem WittVector.sub_coeff {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x y : WittVector p R) (n : β„•) :
                                                                              (x - y).coeff n = peval (wittSub p n) ![x.coeff, y.coeff]
                                                                              source
                                                                              theorem WittVector.mul_coeff {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x y : WittVector p R) (n : β„•) :
                                                                              (x * y).coeff n = peval (wittMul p n) ![x.coeff, y.coeff]
                                                                              source
                                                                              theorem WittVector.neg_coeff {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x : WittVector p R) (n : β„•) :
                                                                              (-x).coeff n = peval (wittNeg p n) ![x.coeff]
                                                                              source
                                                                              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 = peval (wittNSMul p m n) ![x.coeff]
                                                                              source
                                                                              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 = peval (wittZSMul p m n) ![x.coeff]
                                                                              source
                                                                              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 = peval (wittPow p m n) ![x.coeff]
                                                                              source
                                                                              theorem WittVector.add_coeff_zero {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x y : WittVector p R) :
                                                                              (x + y).coeff 0 = x.coeff 0 + y.coeff 0
                                                                              source
                                                                              theorem WittVector.mul_coeff_zero {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x y : WittVector p R) :
                                                                              (x * y).coeff 0 = x.coeff 0 * y.coeff 0
                                                                              source
                                                                              theorem WittVector.wittAdd_vars (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                                                                              (wittAdd p n).vars βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)
                                                                              source
                                                                              theorem WittVector.wittSub_vars (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                                                                              (wittSub p n).vars βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)
                                                                              source
                                                                              theorem WittVector.wittMul_vars (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                                                                              (wittMul p n).vars βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)
                                                                              source
                                                                              theorem WittVector.wittNeg_vars (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                                                                              (wittNeg p n).vars βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)
                                                                              source
                                                                              theorem WittVector.wittNSMul_vars (p : β„•) [hp : Fact (Nat.Prime p)] (m n : β„•) :
                                                                              (wittNSMul p m n).vars βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)
                                                                              source
                                                                              theorem WittVector.wittZSMul_vars (p : β„•) [hp : Fact (Nat.Prime p)] (m : β„€) (n : β„•) :
                                                                              (wittZSMul p m n).vars βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)
                                                                              source
                                                                              theorem WittVector.wittPow_vars (p : β„•) [hp : Fact (Nat.Prime p)] (m n : β„•) :
                                                                              (wittPow p m n).vars βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)