# mathlibdocumentation

ring_theory.witt_vector.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 ring_theory/witt_vector/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 structure_polynomial.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

• witt_vector p R: the type of p-typical Witt vectors with coefficients in R.
• witt_vector.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.

@[nolint]
def witt_vector (p : ) (R : Type u_1) :
Type u_1

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

Equations
def witt_vector.mk (p : ) {R : Type u_1} (x : → R) :
R

Construct a Witt vector mk p x : 𝕎 R from a sequence x of elements of R.

Equations
• = x
@[instance]
def witt_vector.inhabited {p : } {R : Type u_1} [inhabited R] :

Equations
def witt_vector.coeff {p : } {R : Type u_1} (x : R) (n : ) :
R

x.coeff n is the nth coefficient of the Witt vector x.

This concept does not have a standard name in the literature.

Equations
@[ext]
theorem witt_vector.ext {p : } {R : Type u_1} {x y : R} (h : ∀ (n : ), x.coeff n = y.coeff n) :
x = y

theorem witt_vector.ext_iff {p : } {R : Type u_1} {x y : R} :
x = y ∀ (n : ), x.coeff n = y.coeff n

@[simp]
theorem witt_vector.coeff_mk (p : ) {R : Type u_1} (x : → R) :
x).coeff = x

@[instance]
def witt_vector.functor (p : ) :

Equations
• = {map := λ (α β : Type u_1) (f : α → β) (v : α), f v, map_const := λ (α β : Type u_1) (a : α) (v : β) (_x : ), a}
@[instance]

def witt_vector.witt_zero (p : ) [hp : fact (nat.prime p)] :

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

Equations
def witt_vector.witt_one (p : ) [hp : fact (nat.prime p)] :

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

Equations
def witt_vector.witt_add (p : ) [hp : fact (nat.prime p)] :

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

Equations
def witt_vector.witt_sub (p : ) [hp : fact (nat.prime p)] :

The polynomials used for describing the subtraction of the ring of Witt vectors. Note that a - b is defined as a + -b. See witt_vector.sub_coeff for a proof that subtraction is precisely given by these polynomials witt_vector.witt_sub

Equations
def witt_vector.witt_mul (p : ) [hp : fact (nat.prime p)] :

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

Equations
def witt_vector.witt_neg (p : ) [hp : fact (nat.prime p)] :

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

Equations
def witt_vector.peval {R : Type u_1} [comm_ring R] {k : } (φ : mv_polynomial (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.

Equations
def witt_vector.eval {p : } {R : Type u_1} [comm_ring R] {k : } (φ : mv_polynomial (fin k × ) ) (x : fin k R) :
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₁.

Equations
@[instance]
def witt_vector.has_zero {p : } (R : Type u_1) [comm_ring R] [fact (nat.prime p)] :

Equations
@[instance]
def witt_vector.has_one {p : } (R : Type u_1) [comm_ring R] [fact (nat.prime p)] :

Equations
@[instance]
def witt_vector.has_add {p : } (R : Type u_1) [comm_ring R] [fact (nat.prime p)] :

Equations
• = {add := λ (x y : R), ![x, y]}
@[instance]
def witt_vector.has_mul {p : } (R : Type u_1) [comm_ring R] [fact (nat.prime p)] :

Equations
• = {mul := λ (x y : R), ![x, y]}
@[instance]
def witt_vector.has_neg {p : } (R : Type u_1) [comm_ring R] [fact (nat.prime p)] :

Equations
• = {neg := λ (x : R), ![x]}
@[simp]
theorem witt_vector.witt_zero_eq_zero (p : ) [hp : fact (nat.prime p)] (n : ) :

@[simp]
theorem witt_vector.witt_one_zero_eq_one (p : ) [hp : fact (nat.prime p)] :

@[simp]
theorem witt_vector.witt_one_pos_eq_zero (p : ) [hp : fact (nat.prime p)] (n : ) (hn : 0 < n) :

@[simp]
theorem witt_vector.witt_add_zero (p : ) [hp : fact (nat.prime p)] :

@[simp]
theorem witt_vector.witt_sub_zero (p : ) [hp : fact (nat.prime p)] :

@[simp]
theorem witt_vector.witt_mul_zero (p : ) [hp : fact (nat.prime p)] :

@[simp]
theorem witt_vector.witt_neg_zero (p : ) [hp : fact (nat.prime p)] :

@[simp]
theorem witt_vector.constant_coeff_witt_add (p : ) [hp : fact (nat.prime p)] (n : ) :

@[simp]
theorem witt_vector.constant_coeff_witt_sub (p : ) [hp : fact (nat.prime p)] (n : ) :

@[simp]
theorem witt_vector.constant_coeff_witt_mul (p : ) [hp : fact (nat.prime p)] (n : ) :

@[simp]
theorem witt_vector.constant_coeff_witt_neg (p : ) [hp : fact (nat.prime p)] (n : ) :

@[simp]
theorem witt_vector.zero_coeff (p : ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] (n : ) :
0.coeff n = 0

@[simp]
theorem witt_vector.one_coeff_zero (p : ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] :
1.coeff 0 = 1

@[simp]
theorem witt_vector.one_coeff_eq_of_pos (p : ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] (n : ) (hn : 0 < n) :
1.coeff n = 0

theorem witt_vector.add_coeff {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x y : R) (n : ) :
(x + y).coeff n = ![x.coeff, y.coeff]

theorem witt_vector.mul_coeff {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x y : R) (n : ) :
(x * y).coeff n = ![x.coeff, y.coeff]

theorem witt_vector.neg_coeff {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x : R) (n : ) :
(-x).coeff n = ![x.coeff]