Witt vectors over a domain #

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

This file builds to the proof witt_vector.is_domain, an instance that says if R is an integral domain, then so is 𝕎 R. It depends on the API around iterated applications of witt_vector.verschiebung and witt_vector.frobenius found in identities.lean.

The proof sketch goes as follows: any nonzero $x$ is an iterated application of $V$ to some vector $w_x$ whose 0th component is nonzero (witt_vector.verschiebung_nonzero). Known identities (witt_vector.iterate_verschiebung_mul) allow us to transform the product of two such $x$ and $y$ to the form $V^{m+n}\left(F^n(w_x) \cdot F^m(w_y)\right)$, the 0th component of which must be nonzero.

Main declarations #

witt_vector.iterate_verschiebung_mul_coeff : an identity from [Haz09]
witt_vector.is_domain

The `shift` operator #

source

def witt_vector.shift {p : ℕ} {R : Type u_1} (x : witt_vector p R) (n : ℕ) :

witt_vector p R

witt_vector.verschiebung translates the entries of a Witt vector upward, inserting 0s in the gaps. witt_vector.shift does the opposite, removing the first entries. This is mainly useful as an auxiliary construction for witt_vector.verschiebung_nonzero.

Equations

x.shift n = {coeff := λ (i : ℕ), x.coeff (n + i)}

source

theorem witt_vector.shift_coeff {p : ℕ} {R : Type u_1} (x : witt_vector p R) (n k : ℕ) :

(x.shift n).coeff k = x.coeff (n + k)

source

theorem witt_vector.verschiebung_shift {p : ℕ} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x : witt_vector p R) (k : ℕ) (h : ∀ (i : ℕ), i < k + 1 → x.coeff i = 0) :

⇑witt_vector.verschiebung (x.shift k.succ) = x.shift k

source

theorem witt_vector.eq_iterate_verschiebung {p : ℕ} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] {x : witt_vector p R} {n : ℕ} (h : ∀ (i : ℕ), i < n → x.coeff i = 0) :

x = ⇑witt_vector.verschiebung ^[n] (x.shift n)

source

theorem witt_vector.verschiebung_nonzero {p : ℕ} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] {x : witt_vector p R} (hx : x ≠ 0) :

∃ (n : ℕ) (x' : witt_vector p R), x'.coeff 0 ≠ 0 ∧ x = ⇑witt_vector.verschiebung ^[n] x'