Documentation

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 ()] [] (x : ) :
WittVector.frobenius (WittVector.verschiebung x) = x * p

The composition of Frobenius and Verschiebung is multiplication by p.

theorem WittVector.verschiebung_zmod {p : } [hp : Fact ()] (x : WittVector p (ZMod p)) :
WittVector.verschiebung x = x * p

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

theorem WittVector.coeff_p_pow (p : ) (R : Type u_1) [hp : Fact ()] [] [CharP R p] (i : ) :
WittVector.coeff (p ^ i) i = 1
theorem WittVector.coeff_p_pow_eq_zero (p : ) (R : Type u_1) [hp : Fact ()] [] [CharP R p] {i : } {j : } (hj : j i) :
WittVector.coeff (p ^ i) j = 0
theorem WittVector.coeff_p (p : ) (R : Type u_1) [hp : Fact ()] [] [CharP R p] (i : ) :
WittVector.coeff (p) i = if i = 1 then 1 else 0
@[simp]
theorem WittVector.coeff_p_zero (p : ) (R : Type u_1) [hp : Fact ()] [] [CharP R p] :
WittVector.coeff (p) 0 = 0
@[simp]
theorem WittVector.coeff_p_one (p : ) (R : Type u_1) [hp : Fact ()] [] [CharP R p] :
WittVector.coeff (p) 1 = 1
theorem WittVector.p_nonzero (p : ) (R : Type u_1) [hp : Fact ()] [] [] [CharP R p] :
p 0
theorem WittVector.FractionRing.p_nonzero (p : ) (R : Type u_1) [hp : Fact ()] [] [] [CharP R p] :
p 0
theorem WittVector.verschiebung_mul_frobenius {p : } {R : Type u_1} [hp : Fact ()] [] (x : ) (y : ) :
WittVector.verschiebung (x * WittVector.frobenius y) = WittVector.verschiebung x * y

The “projection formula” for Frobenius and Verschiebung.

theorem WittVector.mul_charP_coeff_zero {p : } {R : Type u_1} [hp : Fact ()] [] [CharP R p] (x : ) :
WittVector.coeff (x * p) 0 = 0
theorem WittVector.mul_charP_coeff_succ {p : } {R : Type u_1} [hp : Fact ()] [] [CharP R p] (x : ) (i : ) :
WittVector.coeff (x * p) (i + 1) = ^ p
theorem WittVector.verschiebung_frobenius {p : } {R : Type u_1} [hp : Fact ()] [] [CharP R p] (x : ) :
WittVector.verschiebung (WittVector.frobenius x) = x * p
theorem WittVector.verschiebung_frobenius_comm {p : } {R : Type u_1} [hp : Fact ()] [] [CharP R p] :
Function.Commute WittVector.verschiebung WittVector.frobenius

Iteration lemmas #

theorem WittVector.iterate_verschiebung_coeff {p : } {R : Type u_1} [hp : Fact ()] [] (x : ) (n : ) (k : ) :
WittVector.coeff () (k + n) =
theorem WittVector.iterate_verschiebung_mul_left {p : } {R : Type u_1} [hp : Fact ()] [] (x : ) (y : ) (i : ) :
theorem WittVector.iterate_verschiebung_mul {p : } {R : Type u_1} [hp : Fact ()] [] [CharP R p] (x : ) (y : ) (i : ) (j : ) :
theorem WittVector.iterate_frobenius_coeff {p : } {R : Type u_1} [hp : Fact ()] [] [CharP R p] (x : ) (i : ) (k : ) :
= ^ p ^ i
theorem WittVector.iterate_verschiebung_mul_coeff {p : } {R : Type u_1} [hp : Fact ()] [] [CharP R p] (x : ) (y : ) (i : ) (j : ) :
= ^ p ^ j * ^ p ^ i

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