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
verschiebung_mul_frobenius: the “projection formula”:
V(x * F y) = V x * y
iterate_verschiebung_mul_coeff: an identity from [Haze09] 6.2
[Hazewinkel, Witt Vectors][Haze09]
[Commelin and Lewis, Formalizing the Ring of Witt Vectors][CL21]
Iteration lemmas #
This is a slightly specialized form of [Hazewinkel, Witt Vectors][Haze09] 6.2 equation 5.