mathlib3 documentation

ring_theory.witt_vector.defs

Witt vectors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

References #

structure witt_vector (p : ℕ) (R : Type u_1) :

Type u_1

coeff : ℕ → R

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

@[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

theorem witt_vector.coeff_mk (p : ℕ) {R : Type u_1} (x : ℕ → R) :

{coeff := x}.coeff = x

@[protected, instance]

def witt_vector.functor (p : ℕ) :

functor (witt_vector p)

Equations

witt_vector.functor p = {map := λ (α β : Type u_1) (f : α → β) (v : witt_vector p α), {coeff := f ∘ v.coeff}, map_const := λ (α β : Type u_1) (a : α) (v : witt_vector p β), {coeff := λ (_x : ℕ), a}}

@[protected, instance]

def witt_vector.is_lawful_functor (p : ℕ) :

is_lawful_functor (witt_vector p)

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

witt_vector.witt_zero p = witt_structure_int p 0

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

witt_vector.witt_one p = witt_structure_int p 1

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

witt_vector.witt_add p = witt_structure_int p (mv_polynomial.X 0 + mv_polynomial.X 1)

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

witt_vector.witt_nsmul p n = witt_structure_int p (n • mv_polynomial.X 0)

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

witt_vector.witt_zsmul p n = witt_structure_int p (n • mv_polynomial.X 0)

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

witt_vector.witt_sub p = witt_structure_int p (mv_polynomial.X 0 - mv_polynomial.X 1)

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

witt_vector.witt_mul p = witt_structure_int p (mv_polynomial.X 0 * mv_polynomial.X 1)

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

witt_vector.witt_neg p = witt_structure_int p (-mv_polynomial.X 0)

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

witt_vector.witt_pow p n = witt_structure_int p (mv_polynomial.X 0 ^ n)

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

witt_vector.peval φ x = ⇑(mv_polynomial.aeval (function.uncurry x)) φ

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

witt_vector.eval φ x = {coeff := λ (n : ℕ), witt_vector.peval (φ n) (λ (i : fin k), (x i).coeff)}

@[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

witt_vector.has_zero R = {zero := witt_vector.eval (witt_vector.witt_zero p) matrix.vec_empty}

@[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

witt_vector.inhabited R = {default := 0}

@[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

witt_vector.has_one R = {one := witt_vector.eval (witt_vector.witt_one p) matrix.vec_empty}

@[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

witt_vector.has_add R = {add := λ (x y : witt_vector p R), witt_vector.eval (witt_vector.witt_add p) ![x, y]}

@[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

witt_vector.has_sub R = {sub := λ (x y : witt_vector p R), witt_vector.eval (witt_vector.witt_sub p) ![x, y]}

@[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

witt_vector.has_nat_scalar R = {smul := λ (n : ℕ) (x : witt_vector p R), witt_vector.eval (witt_vector.witt_nsmul p n) ![x]}

@[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

witt_vector.has_int_scalar R = {smul := λ (n : ℤ) (x : witt_vector p R), witt_vector.eval (witt_vector.witt_zsmul p n) ![x]}

@[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

witt_vector.has_mul R = {mul := λ (x y : witt_vector p R), witt_vector.eval (witt_vector.witt_mul p) ![x, y]}

@[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

witt_vector.has_neg R = {neg := λ (x : witt_vector p R), witt_vector.eval (witt_vector.witt_neg p) ![x]}

@[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

witt_vector.has_nat_pow R = {pow := λ (x : witt_vector p R) (n : ℕ), witt_vector.eval (witt_vector.witt_pow p n) ![x]}

@[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

witt_vector.has_nat_cast R = {nat_cast := nat.unary_cast (witt_vector.has_add R)}

@[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

witt_vector.has_int_cast R = {int_cast := int.cast_def (witt_vector.has_neg R)}

@[simp]

theorem witt_vector.witt_zero_eq_zero (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :

witt_vector.witt_zero p n = 0

@[simp]

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

witt_vector.witt_one p 0 = 1

@[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

@[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)

@[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)

@[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)

@[simp]

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

witt_vector.witt_neg p 0 = -mv_polynomial.X (0, 0)

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

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]

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]

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]

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]

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]

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]

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]

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

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

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)

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)

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)

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)

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)

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)

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)