# 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 #

• WittVector p R: the type of p-typical Witt vectors with coefficients in R.
• WittVector.coeff x n: projects the nth value of the Witt vector x.

## 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 : } {y : } (h : β (n : β), x.coeff n = y.coeff n) :
x = y
theorem WittVector.ext_iff {p : β} {R : Type u_1} {x : } {y : } :
x = y β β (n : β), x.coeff n = y.coeff n
theorem WittVector.coeff_mk (p : β) {R : Type u_1} (x : β β R) :
().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} [] {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} [] {k : β} (Ο : β β MvPolynomial (Fin k Γ β) β€) (x : Fin k β ) :

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) [] [Fact ()] :
Zero ()
Equations
• = { zero := }
instance WittVector.instInhabited {p : β} (R : Type u_1) [] [Fact ()] :
Equations
• = { default := 0 }
instance WittVector.instOne {p : β} (R : Type u_1) [] [Fact ()] :
One ()
Equations
• = { one := }
instance WittVector.instAdd {p : β} (R : Type u_1) [] [Fact ()] :
Equations
instance WittVector.instSub {p : β} (R : Type u_1) [] [Fact ()] :
Sub ()
Equations
instance WittVector.hasNatScalar {p : β} (R : Type u_1) [] [Fact ()] :
Equations
instance WittVector.hasIntScalar {p : β} (R : Type u_1) [] [Fact ()] :
Equations
instance WittVector.instMul {p : β} (R : Type u_1) [] [Fact ()] :
Mul ()
Equations
instance WittVector.instNeg {p : β} (R : Type u_1) [] [Fact ()] :
Neg ()
Equations
• = { neg := fun (x : ) => }
instance WittVector.hasNatPow {p : β} (R : Type u_1) [] [Fact ()] :
Equations
instance WittVector.instNatCast {p : β} (R : Type u_1) [] [Fact ()] :
Equations
• = { natCast := Nat.unaryCast }
instance WittVector.instIntCast {p : β} (R : Type u_1) [] [Fact ()] :
Equations
• = { intCast := Int.castDef }
@[simp]
theorem WittVector.wittZero_eq_zero (p : β) [hp : Fact ()] (n : β) :
= 0
@[simp]
theorem WittVector.wittOne_zero_eq_one (p : β) [hp : Fact ()] :
= 1
@[simp]
theorem WittVector.wittOne_pos_eq_zero (p : β) [hp : Fact ()] (n : β) (hn : 0 < n) :
= 0
@[simp]
theorem WittVector.wittAdd_zero (p : β) [hp : Fact ()] :
@[simp]
theorem WittVector.wittSub_zero (p : β) [hp : Fact ()] :
@[simp]
theorem WittVector.wittMul_zero (p : β) [hp : Fact ()] :
@[simp]
theorem WittVector.wittNeg_zero (p : β) [hp : Fact ()] :
@[simp]
theorem WittVector.constantCoeff_wittAdd (p : β) [hp : Fact ()] (n : β) :
MvPolynomial.constantCoeff () = 0
@[simp]
theorem WittVector.constantCoeff_wittSub (p : β) [hp : Fact ()] (n : β) :
MvPolynomial.constantCoeff () = 0
@[simp]
theorem WittVector.constantCoeff_wittMul (p : β) [hp : Fact ()] (n : β) :
MvPolynomial.constantCoeff () = 0
@[simp]
theorem WittVector.constantCoeff_wittNeg (p : β) [hp : Fact ()] (n : β) :
MvPolynomial.constantCoeff () = 0
@[simp]
theorem WittVector.constantCoeff_wittNSMul (p : β) [hp : Fact ()] (m : β) (n : β) :
MvPolynomial.constantCoeff () = 0
@[simp]
theorem WittVector.constantCoeff_wittZSMul (p : β) [hp : Fact ()] (z : β€) (n : β) :
MvPolynomial.constantCoeff () = 0
@[simp]
theorem WittVector.zero_coeff (p : β) (R : Type u_1) [hp : Fact ()] [] (n : β) :
= 0
@[simp]
theorem WittVector.one_coeff_zero (p : β) (R : Type u_1) [hp : Fact ()] [] :
= 1
@[simp]
theorem WittVector.one_coeff_eq_of_pos (p : β) (R : Type u_1) [hp : Fact ()] [] (n : β) (hn : 0 < n) :
= 0
@[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 ()] [] (x : ) (y : ) (n : β) :
(x + y).coeff n = WittVector.peval () ![x.coeff, y.coeff]
theorem WittVector.sub_coeff {p : β} {R : Type u_1} [hp : Fact ()] [] (x : ) (y : ) (n : β) :
(x - y).coeff n = WittVector.peval () ![x.coeff, y.coeff]
theorem WittVector.mul_coeff {p : β} {R : Type u_1} [hp : Fact ()] [] (x : ) (y : ) (n : β) :
(x * y).coeff n = WittVector.peval () ![x.coeff, y.coeff]
theorem WittVector.neg_coeff {p : β} {R : Type u_1} [hp : Fact ()] [] (x : ) (n : β) :
(-x).coeff n = WittVector.peval () ![x.coeff]
theorem WittVector.nsmul_coeff {p : β} {R : Type u_1} [hp : Fact ()] [] (m : β) (x : ) (n : β) :
(m β’ x).coeff n = WittVector.peval () ![x.coeff]
theorem WittVector.zsmul_coeff {p : β} {R : Type u_1} [hp : Fact ()] [] (m : β€) (x : ) (n : β) :
(m β’ x).coeff n = WittVector.peval () ![x.coeff]
theorem WittVector.pow_coeff {p : β} {R : Type u_1} [hp : Fact ()] [] (m : β) (x : ) (n : β) :
(x ^ m).coeff n = WittVector.peval () ![x.coeff]
theorem WittVector.add_coeff_zero {p : β} {R : Type u_1} [hp : Fact ()] [] (x : ) (y : ) :
(x + y).coeff 0 = x.coeff 0 + y.coeff 0
theorem WittVector.mul_coeff_zero {p : β} {R : Type u_1} [hp : Fact ()] [] (x : ) (y : ) :
(x * y).coeff 0 = x.coeff 0 * y.coeff 0
theorem WittVector.wittAdd_vars (p : β) [hp : Fact ()] (n : β) :
().vars β Finset.univ ΓΛ’ Finset.range (n + 1)
theorem WittVector.wittSub_vars (p : β) [hp : Fact ()] (n : β) :
().vars β Finset.univ ΓΛ’ Finset.range (n + 1)
theorem WittVector.wittMul_vars (p : β) [hp : Fact ()] (n : β) :
().vars β Finset.univ ΓΛ’ Finset.range (n + 1)
theorem WittVector.wittNeg_vars (p : β) [hp : Fact ()] (n : β) :
().vars β Finset.univ ΓΛ’ Finset.range (n + 1)
theorem WittVector.wittNSMul_vars (p : β) [hp : Fact ()] (m : β) (n : β) :
().vars β Finset.univ ΓΛ’ Finset.range (n + 1)
theorem WittVector.wittZSMul_vars (p : β) [hp : Fact ()] (m : β€) (n : β) :
().vars β Finset.univ ΓΛ’ Finset.range (n + 1)
theorem WittVector.wittPow_vars (p : β) [hp : Fact ()] (m : β) (n : β) :
().vars β Finset.univ ΓΛ’ Finset.range (n + 1)