# 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 #

def WittVector.teichmullerFun (p : ) {R : Type u_1} [] (r : 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.

Equations
• = { coeff := fun (n : ) => if n = 0 then r else 0 }
Instances For

## 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)] [] :
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.

Equations
• = { toFun := , map_one' := , map_mul' := }
Instances For
@[simp]
theorem WittVector.teichmuller_coeff_zero (p : ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [] (r : R) :
( r).coeff 0 = r
@[simp]
theorem WittVector.teichmuller_coeff_pos (p : ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [] (r : R) (n : ) :
0 < n( r).coeff n = 0
@[simp]
theorem WittVector.teichmuller_zero (p : ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [] :
= 0
@[simp]
theorem WittVector.map_teichmuller (p : ) {R : Type u_1} {S : Type u_2} [hp : Fact (Nat.Prime p)] [] [] (f : R →+* S) (r : R) :
( r) = (f r)

teichmuller is a natural transformation.

@[simp]
theorem WittVector.ghostComponent_teichmuller (p : ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [] (r : R) (n : ) :
( r) = r ^ p ^ n

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