# mathlib3documentation

ring_theory.witt_vector.teichmuller

# Teichmüller lifts #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines witt_vector.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 #

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

## References #

def witt_vector.teichmuller_fun (p : ) {R : Type u_1} [comm_ring R] (r : R) :
R

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

Equations

## teichmuller is a monoid homomorphism #

On ghost components, it is clear that teichmuller_fun 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 mv_polynomial R ℤ,
3. and from that we can prove the result for arbitrary R.
def witt_vector.teichmuller (p : ) {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] :
R →* 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
@[simp]
theorem witt_vector.teichmuller_coeff_zero (p : ) {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (r : R) :
r).coeff 0 = r
@[simp]
theorem witt_vector.teichmuller_coeff_pos (p : ) {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (r : R) (n : ) (hn : 0 < n) :
r).coeff n = 0
@[simp]
theorem witt_vector.teichmuller_zero (p : ) {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] :
= 0
@[simp]
theorem witt_vector.map_teichmuller (p : ) {R : Type u_1} {S : Type u_2} [hp : fact (nat.prime p)] [comm_ring R] [comm_ring S] (f : R →+* S) (r : R) :
r) = (f r)

teichmuller is a natural transformation.

@[simp]
theorem witt_vector.ghost_component_teichmuller (p : ) {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (r : R) (n : ) :
= r ^ p ^ n

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