Mathlib.RingTheory.WittVector.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 [Haze09] 6.2

References #

[Hazewinkel, Witt Vectors][Haze09]
[Commelin and Lewis, Formalizing the Ring of Witt Vectors][CL21]

theorem WittVector.frobenius_verschiebung {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x : WittVector p R) :

frobenius (verschiebung x) = x * ↑p

The composition of Frobenius and Verschiebung is multiplication by p.

source

📐 coverage

theorem WittVector.verschiebung_zmod {p : ℕ} [hp : Fact (Nat.Prime p)] (x : WittVector p (ZMod p)) :

verschiebung x = x * ↑p

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

source

📐 coverage

theorem WittVector.coeff_p_pow (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] (i : ℕ) :

(↑p ^ i).coeff i = 1

source

📐 coverage

theorem WittVector.coeff_p_pow_eq_zero (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] {i j : ℕ} (hj : j ≠ i) :

(↑p ^ i).coeff j = 0

source

📐 coverage

theorem WittVector.coeff_p (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] (i : ℕ) :

(↑p).coeff i = if i = 1 then 1 else 0

source

📐 coverage

@[simp]

theorem WittVector.coeff_p_zero (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] :

(↑p).coeff 0 = 0

source

📐 coverage

@[simp]

theorem WittVector.coeff_p_one (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] :

(↑p).coeff 1 = 1

source

theorem WittVector.p_nonzero (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] [Nontrivial R] [CharP R p] :

↑p ≠ 0

source

theorem WittVector.FractionRing.p_nonzero (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] [Nontrivial R] [CharP R p] :

↑p ≠ 0

source

📐 coverage

theorem WittVector.verschiebung_mul_frobenius {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x y : WittVector p R) :

verschiebung (x * frobenius y) = verschiebung x * y

The “projection formula” for Frobenius and Verschiebung.

source

📐 coverage

theorem WittVector.mul_charP_coeff_zero {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] (x : WittVector p R) :

(x * ↑p).coeff 0 = 0

source

📐 coverage

theorem WittVector.mul_charP_coeff_succ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] (x : WittVector p R) (i : ℕ) :

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

source

📐 coverage

theorem WittVector.mul_pow_charP_coeff_zero {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] (x : WittVector p R) {m n : ℕ} (h : m < n) :

(x * ↑p ^ n).coeff m = 0

source

📐 coverage

theorem WittVector.mul_pow_charP_coeff_succ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] (x : WittVector p R) {m n : ℕ} :

(x * ↑p ^ n).coeff (m + n) = x.coeff m ^ p ^ n

source

📐 coverage

theorem WittVector.verschiebung_frobenius {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] (x : WittVector p R) :

verschiebung (frobenius x) = x * ↑p

source

📐 coverage

theorem WittVector.verschiebung_frobenius_comm {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] :

Function.Commute ⇑verschiebung ⇑frobenius

Iteration lemmas #

source

📐 coverage

theorem WittVector.iterate_verschiebung_coeff_eq_zero {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x : WittVector p R) {n m : ℕ} (h : m < n) :

((⇑verschiebung)^[n] x).coeff m = 0

source

📐 coverage

theorem WittVector.iterate_verschiebung_coeff {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x : WittVector p R) (n k : ℕ) :

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

source

📐 coverage

theorem WittVector.iterate_verschiebung_mul_left {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x y : WittVector p R) (i : ℕ) :

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

source

📐 coverage

theorem WittVector.iterate_verschiebung_mul {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] (x y : WittVector p R) (i j : ℕ) :

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

source

📐 coverage

theorem WittVector.iterate_frobenius_coeff {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] (x : WittVector p R) (i k : ℕ) :

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

source

📐 coverage

theorem WittVector.iterate_verschiebung_mul_coeff {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] (x y : WittVector p R) (i j : ℕ) :

((⇑verschiebung)^[i] x * (⇑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][Haze09] 6.2 equation 5.

source

📐 coverage

theorem WittVector.iterate_verschiebung_iterate_frobenius {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] (x : WittVector p R) (n : ℕ) :

(⇑verschiebung)^[n] ((⇑frobenius)^[n] x) = x * ↑p ^ n