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.

References #

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

Instances for witt_vector
source
@[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
source
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
source
theorem witt_vector.coeff_mk (p : β„•) {R : Type u_1} (x : β„• β†’ R) :
{coeff := x}.coeff = x
source
@[protected, instance]
def witt_vector.functor (p : β„•) :
functor (witt_vector p)
Equations
source
@[protected, instance]
def witt_vector.is_lawful_functor (p : β„•) :
is_lawful_functor (witt_vector p)
source
noncomputable def witt_vector.witt_zero (p : β„•) [hp : fact (nat.prime p)] :
β„• β†’ mv_polynomial (fin 0 Γ— β„•) β„€

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

Equations
source
noncomputable def witt_vector.witt_one (p : β„•) [hp : fact (nat.prime p)] :
β„• β†’ mv_polynomial (fin 0 Γ— β„•) β„€

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

Equations
source
noncomputable def witt_vector.witt_add (p : β„•) [hp : fact (nat.prime p)] :
β„• β†’ mv_polynomial (fin 2 Γ— β„•) β„€

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

Equations
source
noncomputable def witt_vector.witt_nsmul (p : β„•) [hp : fact (nat.prime p)] (n : β„•) :
β„• β†’ mv_polynomial (fin 1 Γ— β„•) β„€

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

Equations
source
noncomputable def witt_vector.witt_zsmul (p : β„•) [hp : fact (nat.prime p)] (n : β„€) :
β„• β†’ mv_polynomial (fin 1 Γ— β„•) β„€

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

Equations
source
noncomputable def witt_vector.witt_sub (p : β„•) [hp : fact (nat.prime p)] :
β„• β†’ mv_polynomial (fin 2 Γ— β„•) β„€

The polynomials used for describing the subtraction of the ring of Witt vectors.

Equations
source
noncomputable def witt_vector.witt_mul (p : β„•) [hp : fact (nat.prime p)] :
β„• β†’ mv_polynomial (fin 2 Γ— β„•) β„€

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

Equations
source
noncomputable def witt_vector.witt_neg (p : β„•) [hp : fact (nat.prime p)] :
β„• β†’ mv_polynomial (fin 1 Γ— β„•) β„€

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

Equations
source
noncomputable def witt_vector.witt_pow (p : β„•) [hp : fact (nat.prime p)] (n : β„•) :
β„• β†’ mv_polynomial (fin 1 Γ— β„•) β„€

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

Equations
source
noncomputable 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
source
noncomputable def witt_vector.eval {p : β„•} {R : Type u_1} [comm_ring R] {k : β„•} (Ο† : β„• β†’ mv_polynomial (fin k Γ— β„•) β„€) (x : fin k β†’ witt_vector p R) :
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
source
@[protected, instance]
noncomputable def witt_vector.has_zero {p : β„•} (R : Type u_1) [comm_ring R] [fact (nat.prime p)] :
has_zero (witt_vector p R)
Equations
source
@[protected, instance]
noncomputable def witt_vector.inhabited {p : β„•} (R : Type u_1) [comm_ring R] [fact (nat.prime p)] :
inhabited (witt_vector p R)
Equations
source
@[protected, instance]
noncomputable def witt_vector.has_one {p : β„•} (R : Type u_1) [comm_ring R] [fact (nat.prime p)] :
has_one (witt_vector p R)
Equations
source
@[protected, instance]
noncomputable def witt_vector.has_add {p : β„•} (R : Type u_1) [comm_ring R] [fact (nat.prime p)] :
has_add (witt_vector p R)
Equations
source
@[protected, instance]
noncomputable def witt_vector.has_sub {p : β„•} (R : Type u_1) [comm_ring R] [fact (nat.prime p)] :
has_sub (witt_vector p R)
Equations
source
@[protected, instance]
noncomputable def witt_vector.has_nat_scalar {p : β„•} (R : Type u_1) [comm_ring R] [fact (nat.prime p)] :
has_smul β„• (witt_vector p R)
Equations
source
@[protected, instance]
noncomputable def witt_vector.has_int_scalar {p : β„•} (R : Type u_1) [comm_ring R] [fact (nat.prime p)] :
has_smul β„€ (witt_vector p R)
Equations
source
@[protected, instance]
noncomputable def witt_vector.has_mul {p : β„•} (R : Type u_1) [comm_ring R] [fact (nat.prime p)] :
has_mul (witt_vector p R)
Equations
source
@[protected, instance]
noncomputable def witt_vector.has_neg {p : β„•} (R : Type u_1) [comm_ring R] [fact (nat.prime p)] :
has_neg (witt_vector p R)
Equations
source
@[protected, instance]
noncomputable def witt_vector.has_nat_pow {p : β„•} (R : Type u_1) [comm_ring R] [fact (nat.prime p)] :
has_pow (witt_vector p R) β„•
Equations
source
@[protected, instance]
noncomputable def witt_vector.has_nat_cast {p : β„•} (R : Type u_1) [comm_ring R] [fact (nat.prime p)] :
has_nat_cast (witt_vector p R)
Equations
source
@[protected, instance]
noncomputable def witt_vector.has_int_cast {p : β„•} (R : Type u_1) [comm_ring R] [fact (nat.prime p)] :
has_int_cast (witt_vector p R)
Equations
source
@[simp]
theorem witt_vector.witt_zero_eq_zero (p : β„•) [hp : fact (nat.prime p)] (n : β„•) :
witt_vector.witt_zero p n = 0
source
@[simp]
theorem witt_vector.witt_one_zero_eq_one (p : β„•) [hp : fact (nat.prime p)] :
witt_vector.witt_one p 0 = 1
source
@[simp]
theorem witt_vector.witt_one_pos_eq_zero (p : β„•) [hp : fact (nat.prime p)] (n : β„•) (hn : 0 < n) :
witt_vector.witt_one p n = 0
source
@[simp]
theorem witt_vector.witt_add_zero (p : β„•) [hp : fact (nat.prime p)] :
witt_vector.witt_add p 0 = mv_polynomial.X (0, 0) + mv_polynomial.X (1, 0)
source
@[simp]
theorem witt_vector.witt_sub_zero (p : β„•) [hp : fact (nat.prime p)] :
witt_vector.witt_sub p 0 = mv_polynomial.X (0, 0) - mv_polynomial.X (1, 0)
source
@[simp]
theorem witt_vector.witt_mul_zero (p : β„•) [hp : fact (nat.prime p)] :
witt_vector.witt_mul p 0 = mv_polynomial.X (0, 0) * mv_polynomial.X (1, 0)
source
@[simp]
theorem witt_vector.witt_neg_zero (p : β„•) [hp : fact (nat.prime p)] :
witt_vector.witt_neg p 0 = -mv_polynomial.X (0, 0)
source
@[simp]
theorem witt_vector.constant_coeff_witt_add (p : β„•) [hp : fact (nat.prime p)] (n : β„•) :
⇑mv_polynomial.constant_coeff (witt_vector.witt_add p n) = 0
source
@[simp]
theorem witt_vector.constant_coeff_witt_sub (p : β„•) [hp : fact (nat.prime p)] (n : β„•) :
⇑mv_polynomial.constant_coeff (witt_vector.witt_sub p n) = 0
source
@[simp]
theorem witt_vector.constant_coeff_witt_mul (p : β„•) [hp : fact (nat.prime p)] (n : β„•) :
⇑mv_polynomial.constant_coeff (witt_vector.witt_mul p n) = 0
source
@[simp]
theorem witt_vector.constant_coeff_witt_neg (p : β„•) [hp : fact (nat.prime p)] (n : β„•) :
⇑mv_polynomial.constant_coeff (witt_vector.witt_neg p n) = 0
source
@[simp]
theorem witt_vector.constant_coeff_witt_nsmul (p : β„•) [hp : fact (nat.prime p)] (m n : β„•) :
⇑mv_polynomial.constant_coeff (witt_vector.witt_nsmul p m n) = 0
source
@[simp]
theorem witt_vector.constant_coeff_witt_zsmul (p : β„•) [hp : fact (nat.prime p)] (z : β„€) (n : β„•) :
⇑mv_polynomial.constant_coeff (witt_vector.witt_zsmul p z n) = 0
source
@[simp]
theorem witt_vector.zero_coeff (p : β„•) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] (n : β„•) :
0.coeff n = 0
source
@[simp]
theorem witt_vector.one_coeff_zero (p : β„•) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] :
1.coeff 0 = 1
source
@[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
source
@[simp]
theorem witt_vector.v2_coeff {p' : β„•} {R' : Type u_1} (x y : witt_vector p' R') (i : fin 2) :
(![x, y] i).coeff = ![x.coeff, y.coeff] i
source
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 : β„•) :
(x + y).coeff n = witt_vector.peval (witt_vector.witt_add p n) ![x.coeff, y.coeff]
source
theorem witt_vector.sub_coeff {p : β„•} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x y : witt_vector p R) (n : β„•) :
(x - y).coeff n = witt_vector.peval (witt_vector.witt_sub p n) ![x.coeff, y.coeff]
source
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 : β„•) :
(x * y).coeff n = witt_vector.peval (witt_vector.witt_mul p n) ![x.coeff, y.coeff]
source
theorem witt_vector.neg_coeff {p : β„•} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x : witt_vector p R) (n : β„•) :
(-x).coeff n = witt_vector.peval (witt_vector.witt_neg p n) ![x.coeff]
source
theorem witt_vector.nsmul_coeff {p : β„•} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (m : β„•) (x : witt_vector p R) (n : β„•) :
(m β€’ x).coeff n = witt_vector.peval (witt_vector.witt_nsmul p m n) ![x.coeff]
source
theorem witt_vector.zsmul_coeff {p : β„•} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (m : β„€) (x : witt_vector p R) (n : β„•) :
(m β€’ x).coeff n = witt_vector.peval (witt_vector.witt_zsmul p m n) ![x.coeff]
source
theorem witt_vector.pow_coeff {p : β„•} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (m : β„•) (x : witt_vector p R) (n : β„•) :
(x ^ m).coeff n = witt_vector.peval (witt_vector.witt_pow p m n) ![x.coeff]
source
theorem witt_vector.add_coeff_zero {p : β„•} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x y : witt_vector p R) :
(x + y).coeff 0 = x.coeff 0 + y.coeff 0
source
theorem witt_vector.mul_coeff_zero {p : β„•} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x y : witt_vector p R) :
(x * y).coeff 0 = x.coeff 0 * y.coeff 0
source
theorem witt_vector.witt_add_vars (p : β„•) [hp : fact (nat.prime p)] (n : β„•) :
(witt_vector.witt_add p n).vars βŠ† finset.univ Γ—Λ’ finset.range (n + 1)
source
theorem witt_vector.witt_sub_vars (p : β„•) [hp : fact (nat.prime p)] (n : β„•) :
(witt_vector.witt_sub p n).vars βŠ† finset.univ Γ—Λ’ finset.range (n + 1)
source
theorem witt_vector.witt_mul_vars (p : β„•) [hp : fact (nat.prime p)] (n : β„•) :
(witt_vector.witt_mul p n).vars βŠ† finset.univ Γ—Λ’ finset.range (n + 1)
source
theorem witt_vector.witt_neg_vars (p : β„•) [hp : fact (nat.prime p)] (n : β„•) :
(witt_vector.witt_neg p n).vars βŠ† finset.univ Γ—Λ’ finset.range (n + 1)
source
theorem witt_vector.witt_nsmul_vars (p : β„•) [hp : fact (nat.prime p)] (m n : β„•) :
(witt_vector.witt_nsmul p m n).vars βŠ† finset.univ Γ—Λ’ finset.range (n + 1)
source
theorem witt_vector.witt_zsmul_vars (p : β„•) [hp : fact (nat.prime p)] (m : β„€) (n : β„•) :
(witt_vector.witt_zsmul p m n).vars βŠ† finset.univ Γ—Λ’ finset.range (n + 1)
source
theorem witt_vector.witt_pow_vars (p : β„•) [hp : fact (nat.prime p)] (m n : β„•) :
(witt_vector.witt_pow p m n).vars βŠ† finset.univ Γ—Λ’ finset.range (n + 1)