mathlib3 documentation

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 #

References #

source
def witt_vector.teichmuller_fun (p : ℕ) {R : Type u_1} [comm_ring R] (r : R) :
witt_vector p 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.
source
def witt_vector.teichmuller (p : ℕ) {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] :
R →* witt_vector 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
source
@[simp]
theorem witt_vector.teichmuller_coeff_zero (p : ℕ) {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (r : R) :
(⇑(witt_vector.teichmuller p) r).coeff 0 = r
source
@[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) :
(⇑(witt_vector.teichmuller p) r).coeff n = 0
source
@[simp]
theorem witt_vector.teichmuller_zero (p : ℕ) {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] :
⇑(witt_vector.teichmuller p) 0 = 0
source
@[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) :
⇑(witt_vector.map f) (⇑(witt_vector.teichmuller p) r) = ⇑(witt_vector.teichmuller p) (⇑f r)

teichmuller is a natural transformation.

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

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