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 #

References #

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

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)) :
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 (Nat.Prime p)] [CommRing R] [CharP R p] (i : ) :
WittVector.coeff (p ^ i) i = 1
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) :
WittVector.coeff (p ^ i) j = 0
theorem WittVector.coeff_p (p : ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] [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 (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) :
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 (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 {p : } {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] (x : WittVector p R) :
WittVector.verschiebung (WittVector.frobenius x) = x * 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 #

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