# mathlibdocumentation

ring_theory.witt_vector.domain

# Witt vectors over a domain #

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 #

def witt_vector.shift {p : β} {R : Type u_1} (x : R) (n : β) :
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
theorem witt_vector.shift_coeff {p : β} {R : Type u_1} (x : R) (n k : β) :
(x.shift n).coeff k = x.coeff (n + k)
theorem witt_vector.verschiebung_shift {p : β} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x : R) (k : β) (h : β (i : β), i < k + 1 β x.coeff i = 0) :
= x.shift k
theorem witt_vector.eq_iterate_verschiebung {p : β} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] {x : R} {n : β} (h : β (i : β), i < n β x.coeff i = 0) :
x =
theorem witt_vector.verschiebung_nonzero {p : β} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] {x : R} (hx : x β  0) :
β (n : β) (x' : R), x'.coeff 0 β  0 β§

## Witt vectors over a domain #

If R is an integral domain, then so is π R. This argument is adapted from https://math.stackexchange.com/questions/4117247/ring-of-witt-vectors-over-an-integral-domain/4118723#4118723.

@[protected, instance]
def witt_vector.no_zero_divisors {p : β} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] [ p]  :
@[protected, instance]
def witt_vector.is_domain {p : β} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] [ p] [is_domain R] :