mathlib documentation

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

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) :

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

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

Equations
def witt_vector.coeff {p : β„•} {R : Type u_1} (x : witt_vector p 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 : witt_vector p R} (h : βˆ€ (n : β„•), x.coeff n = y.coeff n) :
x = y

theorem witt_vector.ext_iff {p : β„•} {R : Type u_1} {x y : witt_vector p R} :
x = y ↔ βˆ€ (n : β„•), x.coeff n = y.coeff n

@[simp]
theorem witt_vector.coeff_mk (p : β„•) {R : Type u_1} (x : β„• β†’ R) :

@[instance]

Equations

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

Equations

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

Equations

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

Equations

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

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

Equations

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 β†’ witt_vector 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₁.

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

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

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

Equations
@[simp]

@[simp]
theorem witt_vector.witt_one_pos_eq_zero (p : β„•) [hp : fact (nat.prime p)] (n : β„•) (hn : 0 < 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 : witt_vector p R) (n : β„•) :

theorem witt_vector.mul_coeff {p : β„•} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x y : witt_vector p R) (n : β„•) :

theorem witt_vector.neg_coeff {p : β„•} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x : witt_vector p R) (n : β„•) :