# mathlibdocumentation

ring_theory.witt_vector.identities

## Identities between operations on the ring of Witt vectors #

In this file we derive common identities between the Frobenius and Verschiebung operators.

## Main declarations #

• frobenius_verschiebung: the composition of Frobenius and Verschiebung is multiplication by p
• verschiebung_mul_frobenius: the “projection formula”: V(x * F y) = V x * y
• iterate_verschiebung_mul_coeff: an identity from [Haz09] 6.2

## References #

theorem witt_vector.frobenius_verschiebung {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x : R) :

The composition of Frobenius and Verschiebung is multiplication by p.

theorem witt_vector.verschiebung_zmod {p : } [hp : fact (nat.prime p)] (x : (zmod p)) :

Verschiebung is the same as multiplication by p on the ring of Witt vectors of zmod p.

theorem witt_vector.coeff_p_pow (p : ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [ p] (i : ) :
(p ^ i).coeff i = 1
theorem witt_vector.coeff_p_pow_eq_zero (p : ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [ p] {i j : } (hj : j i) :
(p ^ i).coeff j = 0
theorem witt_vector.coeff_p (p : ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [ p] (i : ) :
p.coeff i = ite (i = 1) 1 0
@[simp]
theorem witt_vector.coeff_p_zero (p : ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [ p] :
p.coeff 0 = 0
@[simp]
theorem witt_vector.coeff_p_one (p : ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [ p] :
p.coeff 1 = 1
theorem witt_vector.p_nonzero (p : ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [nontrivial R] [ p] :
p 0
theorem witt_vector.fraction_ring.p_nonzero (p : ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [nontrivial R] [ p] :
p 0
theorem witt_vector.verschiebung_mul_frobenius {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x y : R) :

The “projection formula” for Frobenius and Verschiebung.

theorem witt_vector.mul_char_p_coeff_zero {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] [ p] (x : R) :
(x * p).coeff 0 = 0
theorem witt_vector.mul_char_p_coeff_succ {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] [ p] (x : R) (i : ) :
(x * p).coeff (i + 1) = x.coeff i ^ p
theorem witt_vector.verschiebung_frobenius {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] [ p] (x : R) :
theorem witt_vector.verschiebung_frobenius_comm {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] [ p] :

## Iteration lemmas #

theorem witt_vector.iterate_verschiebung_coeff {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x : R) (n k : ) :
(k + n) = x.coeff k
theorem witt_vector.iterate_verschiebung_mul_left {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x y : R) (i : ) :
theorem witt_vector.iterate_verschiebung_mul {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] [ p] (x y : R) (i j : ) :
theorem witt_vector.iterate_frobenius_coeff {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] [ p] (x : R) (i k : ) :
= x.coeff k ^ p ^ i
theorem witt_vector.iterate_verschiebung_mul_coeff {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] [ p] (x y : R) (i j : ) :
(i + j) = x.coeff 0 ^ p ^ j * y.coeff 0 ^ p ^ i

This is a slightly specialized form of Hazewinkel, Witt Vectors 6.2 equation 5.