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 [Haz09] 6.2
The composition of Frobenius and Verschiebung is multiplication by
Verschiebung is the same as multiplication by
p on the ring of Witt vectors of
The “projection formula” for Frobenius and Verschiebung.