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 #

References #

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

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

    Instances For
      theorem WittVector.teichmuller_coeff_zero (p : ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (r : R) :
      theorem WittVector.teichmuller_coeff_pos (p : ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (r : R) (n : ) :
      theorem WittVector.teichmuller_zero (p : ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :
      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) :

      teichmuller is a natural transformation.

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

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