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 #

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

    Instances For
      source
      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
      source
      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
      source
      theorem WittVector.coeff_mk (p : β„•) {R : Type u_1} (x : β„• β†’ R) :
      (WittVector.mk p x).coeff = x
      source
      instance WittVector.instFunctorWittVector (p : β„•) :
      Functor (WittVector p)
      source
      instance WittVector.instLawfulFunctorWittVectorInstFunctorWittVector (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.

      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.

        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.

          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.

            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.

              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.

                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.

                  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.

                    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.

                      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 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
                          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 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
                            source
                            instance WittVector.instZeroWittVector {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            Zero (WittVector p R)
                            source
                            instance WittVector.instInhabitedWittVector {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            Inhabited (WittVector p R)
                            source
                            instance WittVector.instOneWittVector {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            One (WittVector p R)
                            source
                            instance WittVector.instAddWittVector {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            Add (WittVector p R)
                            source
                            instance WittVector.instSubWittVector {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            Sub (WittVector p R)
                            source
                            instance WittVector.hasNatScalar {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            SMul β„• (WittVector p R)
                            source
                            instance WittVector.hasIntScalar {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            SMul β„€ (WittVector p R)
                            source
                            instance WittVector.instMulWittVector {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            Mul (WittVector p R)
                            source
                            instance WittVector.instNegWittVector {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            Neg (WittVector p R)
                            source
                            instance WittVector.hasNatPow {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            Pow (WittVector p R) β„•
                            source
                            instance WittVector.instNatCastWittVector {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            NatCast (WittVector p R)
                            source
                            instance WittVector.instIntCastWittVector {p : β„•} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] :
                            IntCast (WittVector p R)
                            source
                            @[simp]
                            theorem WittVector.wittZero_eq_zero (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                            WittVector.wittZero p n = 0
                            source
                            @[simp]
                            theorem WittVector.wittOne_zero_eq_one (p : β„•) [hp : Fact (Nat.Prime p)] :
                            WittVector.wittOne p 0 = 1
                            source
                            @[simp]
                            theorem WittVector.wittOne_pos_eq_zero (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) (hn : 0 < n) :
                            WittVector.wittOne p n = 0
                            source
                            @[simp]
                            theorem WittVector.wittAdd_zero (p : β„•) [hp : Fact (Nat.Prime p)] :
                            WittVector.wittAdd p 0 = MvPolynomial.X (0, 0) + MvPolynomial.X (1, 0)
                            source
                            @[simp]
                            theorem WittVector.wittSub_zero (p : β„•) [hp : Fact (Nat.Prime p)] :
                            WittVector.wittSub p 0 = MvPolynomial.X (0, 0) - MvPolynomial.X (1, 0)
                            source
                            @[simp]
                            theorem WittVector.wittMul_zero (p : β„•) [hp : Fact (Nat.Prime p)] :
                            WittVector.wittMul p 0 = MvPolynomial.X (0, 0) * MvPolynomial.X (1, 0)
                            source
                            @[simp]
                            theorem WittVector.wittNeg_zero (p : β„•) [hp : Fact (Nat.Prime p)] :
                            WittVector.wittNeg p 0 = -MvPolynomial.X (0, 0)
                            source
                            @[simp]
                            theorem WittVector.constantCoeff_wittAdd (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                            ↑MvPolynomial.constantCoeff (WittVector.wittAdd p n) = 0
                            source
                            @[simp]
                            theorem WittVector.constantCoeff_wittSub (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                            ↑MvPolynomial.constantCoeff (WittVector.wittSub p n) = 0
                            source
                            @[simp]
                            theorem WittVector.constantCoeff_wittMul (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                            ↑MvPolynomial.constantCoeff (WittVector.wittMul p n) = 0
                            source
                            @[simp]
                            theorem WittVector.constantCoeff_wittNeg (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                            ↑MvPolynomial.constantCoeff (WittVector.wittNeg p n) = 0
                            source
                            @[simp]
                            theorem WittVector.constantCoeff_wittNSMul (p : β„•) [hp : Fact (Nat.Prime p)] (m : β„•) (n : β„•) :
                            ↑MvPolynomial.constantCoeff (WittVector.wittNSMul p m n) = 0
                            source
                            @[simp]
                            theorem WittVector.constantCoeff_wittZSMul (p : β„•) [hp : Fact (Nat.Prime p)] (z : β„€) (n : β„•) :
                            ↑MvPolynomial.constantCoeff (WittVector.wittZSMul p z n) = 0
                            source
                            @[simp]
                            theorem WittVector.zero_coeff (p : β„•) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] (n : β„•) :
                            WittVector.coeff 0 n = 0
                            source
                            @[simp]
                            theorem WittVector.one_coeff_zero (p : β„•) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] :
                            WittVector.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) :
                            WittVector.coeff 1 n = 0
                            source
                            @[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
                            source
                            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]
                            source
                            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]
                            source
                            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]
                            source
                            theorem WittVector.neg_coeff {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x : WittVector p R) (n : β„•) :
                            WittVector.coeff (-x) n = WittVector.peval (WittVector.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 : β„•) :
                            WittVector.coeff (m β€’ x) n = WittVector.peval (WittVector.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 : β„•) :
                            WittVector.coeff (m β€’ x) n = WittVector.peval (WittVector.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 : β„•) :
                            WittVector.coeff (x ^ m) n = WittVector.peval (WittVector.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 : WittVector p R) (y : WittVector p R) :
                            WittVector.coeff (x + y) 0 = WittVector.coeff x 0 + WittVector.coeff y 0
                            source
                            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) :
                            WittVector.coeff (x * y) 0 = WittVector.coeff x 0 * WittVector.coeff y 0
                            source
                            theorem WittVector.wittAdd_vars (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                            MvPolynomial.vars (WittVector.wittAdd p n) βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)
                            source
                            theorem WittVector.wittSub_vars (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                            MvPolynomial.vars (WittVector.wittSub p n) βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)
                            source
                            theorem WittVector.wittMul_vars (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                            MvPolynomial.vars (WittVector.wittMul p n) βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)
                            source
                            theorem WittVector.wittNeg_vars (p : β„•) [hp : Fact (Nat.Prime p)] (n : β„•) :
                            MvPolynomial.vars (WittVector.wittNeg p n) βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)
                            source
                            theorem WittVector.wittNSMul_vars (p : β„•) [hp : Fact (Nat.Prime p)] (m : β„•) (n : β„•) :
                            MvPolynomial.vars (WittVector.wittNSMul p m n) βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)
                            source
                            theorem WittVector.wittZSMul_vars (p : β„•) [hp : Fact (Nat.Prime p)] (m : β„€) (n : β„•) :
                            MvPolynomial.vars (WittVector.wittZSMul p m n) βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)
                            source
                            theorem WittVector.wittPow_vars (p : β„•) [hp : Fact (Nat.Prime p)] (m : β„•) (n : β„•) :
                            MvPolynomial.vars (WittVector.wittPow p m n) βŠ† Finset.univ Γ—Λ’ Finset.range (n + 1)