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
      theorem WittVector.coeff_surjective {p : β„•} {R : Type u_1} (n : β„•) :
      Function.Surjective fun (x : WittVector p R) => x.coeff n
      source
      @[simp]
      theorem WittVector.coeff_mk (p : β„•) {R : Type u_1} (x : β„• β†’ R) :
      (mk p x).coeff = x
      source
      @[implicit_reducible]
      instance WittVector.instFunctor (p : β„•) :
      Functor (WittVector p)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      instance WittVector.instLawfulFunctor (p : β„•) :
      LawfulFunctor (WittVector p)
      source
      noncomputable 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
        noncomputable 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
          noncomputable 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
            noncomputable 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
              noncomputable 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
                noncomputable 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
                  noncomputable 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
                    noncomputable 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
                      noncomputable 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
                        noncomputable 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
                          noncomputable 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
                            @[implicit_reducible]
                            noncomputable instance WittVector.instZero {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                            Zero (WittVector p R)
                            Equations
                            source
                            @[implicit_reducible]
                            noncomputable instance WittVector.instInhabited {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                            Inhabited (WittVector p R)
                            Equations
                            source
                            @[implicit_reducible]
                            noncomputable instance WittVector.instOne {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                            One (WittVector p R)
                            Equations
                            source
                            @[implicit_reducible]
                            noncomputable instance WittVector.instAdd {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                            Add (WittVector p R)
                            Equations
                            source
                            @[implicit_reducible]
                            noncomputable instance WittVector.instSub {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                            Sub (WittVector p R)
                            Equations
                            source
                            @[implicit_reducible]
                            noncomputable instance WittVector.hasNatScalar {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                            SMul β„• (WittVector p R)
                            Equations
                            source
                            @[implicit_reducible]
                            noncomputable instance WittVector.hasIntScalar {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                            SMul β„€ (WittVector p R)
                            Equations
                            source
                            @[implicit_reducible]
                            noncomputable instance WittVector.instMul {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                            Mul (WittVector p R)
                            Equations
                            source
                            @[implicit_reducible]
                            noncomputable instance WittVector.instNeg {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                            Neg (WittVector p R)
                            Equations
                            source
                            @[implicit_reducible]
                            noncomputable instance WittVector.hasNatPow {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                            Pow (WittVector p R) β„•
                            Equations
                            source
                            @[implicit_reducible]
                            noncomputable instance WittVector.instNatCast {p : β„•} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
                            NatCast (WittVector p R)
                            Equations
                            source
                            @[implicit_reducible]
                            noncomputable 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)