mathlib documentation


Teichmüller lifts #

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 #

References #

def witt_vector.teichmuller_fun (p : ) {R : Type u_1} [comm_ring 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.


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 ( p)] [comm_ring 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.

theorem witt_vector.teichmuller_coeff_zero (p : ) {R : Type u_1} [hp : fact ( p)] [comm_ring R] (r : R) :
theorem witt_vector.teichmuller_coeff_pos (p : ) {R : Type u_1} [hp : fact ( p)] [comm_ring R] (r : R) (n : ) (hn : 0 < n) :
theorem witt_vector.teichmuller_zero (p : ) {R : Type u_1} [hp : fact ( p)] [comm_ring R] :
theorem witt_vector.map_teichmuller (p : ) {R : Type u_1} {S : Type u_2} [hp : fact ( p)] [comm_ring R] [comm_ring S] (f : R →+* S) (r : R) :

teichmuller is a natural transformation.

theorem witt_vector.ghost_component_teichmuller (p : ) {R : Type u_1} [hp : fact ( p)] [comm_ring R] (r : R) (n : ) :

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