ring_theory.witt_vector.identities

Identities between operations on the ring of Witt vectors #

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

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 : witt_vector p R) :

⇑witt_vector.frobenius (⇑witt_vector.verschiebung x) = x * ↑p

The composition of Frobenius and Verschiebung is multiplication by p.

source

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

⇑witt_vector.verschiebung x = x * ↑p

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

source

theorem witt_vector.coeff_p_pow (p : ℕ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [char_p R p] (i : ℕ) :

(↑p ^ i).coeff i = 1

source

theorem witt_vector.coeff_p_pow_eq_zero (p : ℕ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [char_p R p] {i j : ℕ} (hj : j ≠ i) :

(↑p ^ i).coeff j = 0

source

theorem witt_vector.coeff_p (p : ℕ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [char_p R p] (i : ℕ) :

↑p.coeff i = ite (i = 1) 1 0

source

@[simp]

theorem witt_vector.coeff_p_zero (p : ℕ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [char_p R p] :

↑p.coeff 0 = 0

source

@[simp]

theorem witt_vector.coeff_p_one (p : ℕ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [char_p R p] :

↑p.coeff 1 = 1

source

theorem witt_vector.p_nonzero (p : ℕ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [nontrivial R] [char_p R p] :

↑p ≠ 0

source

theorem witt_vector.fraction_ring.p_nonzero (p : ℕ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [nontrivial R] [char_p R p] :

↑p ≠ 0

source

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

⇑witt_vector.verschiebung (x * ⇑witt_vector.frobenius y) = ⇑witt_vector.verschiebung x * y

The “projection formula” for Frobenius and Verschiebung.

source

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

(x * ↑p).coeff 0 = 0

source

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

(x * ↑p).coeff (i + 1) = x.coeff i ^ p

source

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

⇑witt_vector.verschiebung (⇑witt_vector.frobenius x) = x * ↑p

source

theorem witt_vector.verschiebung_frobenius_comm {p : ℕ} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] [char_p R p] :

function.commute ⇑witt_vector.verschiebung ⇑witt_vector.frobenius

Iteration lemmas #

source

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

(⇑witt_vector.verschiebung ^[n] x).coeff (k + n) = x.coeff k

source

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

⇑witt_vector.verschiebung ^[i] x * y = ⇑witt_vector.verschiebung ^[i] (x * ⇑witt_vector.frobenius ^[i] y)

source

theorem witt_vector.iterate_verschiebung_mul {p : ℕ} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] [char_p R p] (x y : witt_vector p R) (i j : ℕ) :

⇑witt_vector.verschiebung ^[i] x * ⇑witt_vector.verschiebung ^[j] y = ⇑witt_vector.verschiebung ^[i + j] (⇑witt_vector.frobenius ^[j] x * ⇑witt_vector.frobenius ^[i] y)

source

theorem witt_vector.iterate_frobenius_coeff {p : ℕ} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] [char_p R p] (x : witt_vector p R) (i k : ℕ) :

(⇑witt_vector.frobenius ^[i] x).coeff k = x.coeff k ^ p ^ i

source

theorem witt_vector.iterate_verschiebung_mul_coeff {p : ℕ} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] [char_p R p] (x y : witt_vector p R) (i j : ℕ) :

(⇑witt_vector.verschiebung ^[i] x * ⇑witt_vector.verschiebung ^[j] y).coeff (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.