Teichmüller lifts

This file defines WittVector.teichmuller, a monoid hom R →* 𝕎 R, which embeds r : R as the 0-th component of a Witt vector whose other coefficients are 0.

Main declarations

• WittVector.teichmuller: the Teichmuller map.
• WittVector.map_teichmuller: WittVector.teichmuller is a natural transformation.
• WittVector.ghostComponent_teichmuller: the n-th ghost component of WittVector.teichmuller p r is r ^ p ^ n.

References

• [Hazewinkel, Witt Vectors][Haze09]

• [Commelin and Lewis, Formalizing the Ring of Witt Vectors][CL21]

def WittVector.teichmullerFun (p : ℕ) {R : Type u_1} [CommRing R] (r : R) : WittVector p R

The underlying function of the monoid hom WittVector.teichmuller. The 0-th coefficient of teichmullerFun p r is r, and all others are 0.

teichmuller is a monoid homomorphism

On ghost components, it is clear that teichmullerFun is a monoid homomorphism. But in general the ghost map is not injective. We follow the same strategy as for proving that the ring operations on 𝕎 R satisfy the ring axioms.

1. We first prove it for rings R where p is invertible, because then the ghost map is in fact an isomorphism.
2. After that, we derive the result for MvPolynomial R ℤ,
3. and from that we can prove the result for arbitrary R.

def WittVector.teichmuller (p : ℕ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] : R →* WittVector p R

The Teichmüller lift of an element of R to 𝕎 R. The 0-th coefficient of teichmuller p r is r, and all others are 0. This is a monoid homomorphism.

@[simp]

theorem WittVector.teichmuller_coeff_zero (p : ℕ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (r : R) : ((teichmuller p) r).coeff 0 = r

@[simp]

theorem WittVector.teichmuller_coeff_pos (p : ℕ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (r : R) (n : ℕ) : 0 < n → ((teichmuller p) r).coeff n = 0

@[simp]

theorem WittVector.teichmuller_zero (p : ℕ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] : (teichmuller p) 0 = 0

@[simp]

theorem WittVector.map_teichmuller (p : ℕ) {R : Type u_1} {S : Type u_2} [hp : Fact (Nat.Prime p)] [CommRing R] [CommRing S] (f : R →+* S) (r : R) : (map f) ((teichmuller p) r) = (teichmuller p) (f r)

teichmuller is a natural transformation.

@[simp]

theorem WittVector.ghostComponent_teichmuller (p : ℕ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (r : R) (n : ℕ) : (ghostComponent n) ((teichmuller p) r) = r ^ p ^ n

The n-th ghost component of teichmuller p r is r ^ p ^ n.