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 bypverschiebung_mul_frobenius: the “projection formula”:V(x * F y) = V x * yiterate_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)
:
The composition of Frobenius and Verschiebung is multiplication by p.
theorem
WittVector.verschiebung_zmod
{p : ℕ}
[hp : Fact (Nat.Prime p)]
(x : WittVector p (ZMod p))
:
Verschiebung is the same as multiplication by p on the ring of Witt vectors of ZMod p.
@[simp]
theorem
WittVector.coeff_p_zero
(p : ℕ)
(R : Type u_1)
[hp : Fact (Nat.Prime p)]
[CommRing R]
[CharP R p]
:
WittVector.coeff (↑p) 0 = 0
@[simp]
theorem
WittVector.coeff_p_one
(p : ℕ)
(R : Type u_1)
[hp : Fact (Nat.Prime p)]
[CommRing R]
[CharP R p]
:
WittVector.coeff (↑p) 1 = 1
theorem
WittVector.p_nonzero
(p : ℕ)
(R : Type u_1)
[hp : Fact (Nat.Prime p)]
[CommRing R]
[Nontrivial R]
[CharP R p]
:
↑p ≠ 0
theorem
WittVector.FractionRing.p_nonzero
(p : ℕ)
(R : Type u_1)
[hp : Fact (Nat.Prime p)]
[CommRing R]
[Nontrivial R]
[CharP R p]
:
↑p ≠ 0
theorem
WittVector.verschiebung_mul_frobenius
{p : ℕ}
{R : Type u_1}
[hp : Fact (Nat.Prime p)]
[CommRing R]
(x : WittVector p R)
(y : WittVector p R)
:
The “projection formula” for Frobenius and Verschiebung.
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)
:
WittVector.coeff (x * ↑p) 0 = 0
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 : ℕ)
:
WittVector.coeff (x * ↑p) (i + 1) = WittVector.coeff x i ^ p
theorem
WittVector.verschiebung_frobenius_comm
{p : ℕ}
{R : Type u_1}
[hp : Fact (Nat.Prime p)]
[CommRing R]
[CharP R p]
:
Function.Commute ↑WittVector.verschiebung ↑WittVector.frobenius
Iteration lemmas #
theorem
WittVector.iterate_verschiebung_coeff
{p : ℕ}
{R : Type u_1}
[hp : Fact (Nat.Prime p)]
[CommRing R]
(x : WittVector p R)
(n : ℕ)
(k : ℕ)
:
WittVector.coeff ((↑WittVector.verschiebung)^[n] x) (k + n) = WittVector.coeff x k
theorem
WittVector.iterate_verschiebung_mul_left
{p : ℕ}
{R : Type u_1}
[hp : Fact (Nat.Prime p)]
[CommRing R]
(x : WittVector p R)
(y : WittVector p R)
(i : ℕ)
:
theorem
WittVector.iterate_verschiebung_mul
{p : ℕ}
{R : Type u_1}
[hp : Fact (Nat.Prime p)]
[CommRing R]
[CharP R p]
(x : WittVector p R)
(y : WittVector p R)
(i : ℕ)
(j : ℕ)
:
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 : ℕ)
:
WittVector.coeff ((↑WittVector.frobenius)^[i] x) k = WittVector.coeff x k ^ p ^ i
theorem
WittVector.iterate_verschiebung_mul_coeff
{p : ℕ}
{R : Type u_1}
[hp : Fact (Nat.Prime p)]
[CommRing R]
[CharP R p]
(x : WittVector p R)
(y : WittVector p R)
(i : ℕ)
(j : ℕ)
:
WittVector.coeff ((↑WittVector.verschiebung)^[i] x * (↑WittVector.verschiebung)^[j] y) (i + j) = WittVector.coeff x 0 ^ p ^ j * WittVector.coeff y 0 ^ p ^ i
This is a slightly specialized form of [Hazewinkel, Witt Vectors][Haze09] 6.2 equation 5.