# Witt vectors #

This file verifies that the ring operations on WittVector p R satisfy the axioms of a commutative ring.

## Main definitions #

• WittVector.map: lifts a ring homomorphism R →+* S to a ring homomorphism 𝕎 R →+* 𝕎 S.
• WittVector.ghostComponent n x: evaluates the nth Witt polynomial on the first n coefficients of x, producing a value in R. This is a ring homomorphism.
• WittVector.ghostMap: a ring homomorphism 𝕎 R →+* (ℕ → R), obtained by packaging all the ghost components together. If p is invertible in R, then the ghost map is an equivalence, which we use to define the ring operations on 𝕎 R.
• WittVector.CommRing: the ring structure induced by the ghost components.

## Notation #

We use notation 𝕎 R, entered \bbW, for the Witt vectors over R.

## Implementation details #

As we prove that the ghost components respect the ring operations, we face a number of repetitive proofs. To avoid duplicating code we factor these proofs into a custom tactic, only slightly more powerful than a tactic macro. This tactic is not particularly useful outside of its applications in this file.

## References #

• [Hazewinkel, Witt Vectors][Haze09]

• [Commelin and Lewis, Formalizing the Ring of Witt Vectors][CL21]

def WittVector.mapFun {p : } {α : Type u_4} {β : Type u_5} (f : αβ) :

f : α → β induces a map from 𝕎 α to 𝕎 β by applying f componentwise. If f is a ring homomorphism, then so is f, see WittVector.map f.

Equations
Instances For
theorem WittVector.mapFun.injective {p : } {α : Type u_4} {β : Type u_5} (f : αβ) (hf : ) :
theorem WittVector.mapFun.surjective {p : } {α : Type u_4} {β : Type u_5} (f : αβ) (hf : ) :

Auxiliary tactic for showing that mapFun respects the ring operations.

Equations
Instances For
theorem WittVector.mapFun.zero {p : } {R : Type u_1} {S : Type u_2} [hp : Fact ()] [] [] (f : R →+* S) :
WittVector.mapFun (f) 0 = 0
theorem WittVector.mapFun.one {p : } {R : Type u_1} {S : Type u_2} [hp : Fact ()] [] [] (f : R →+* S) :
WittVector.mapFun (f) 1 = 1
theorem WittVector.mapFun.add {p : } {R : Type u_1} {S : Type u_2} [hp : Fact ()] [] [] (f : R →+* S) (x : ) (y : ) :
WittVector.mapFun (f) (x + y) = WittVector.mapFun (f) x + WittVector.mapFun (f) y
theorem WittVector.mapFun.sub {p : } {R : Type u_1} {S : Type u_2} [hp : Fact ()] [] [] (f : R →+* S) (x : ) (y : ) :
WittVector.mapFun (f) (x - y) = WittVector.mapFun (f) x - WittVector.mapFun (f) y
theorem WittVector.mapFun.mul {p : } {R : Type u_1} {S : Type u_2} [hp : Fact ()] [] [] (f : R →+* S) (x : ) (y : ) :
WittVector.mapFun (f) (x * y) = WittVector.mapFun (f) x * WittVector.mapFun (f) y
theorem WittVector.mapFun.neg {p : } {R : Type u_1} {S : Type u_2} [hp : Fact ()] [] [] (f : R →+* S) (x : ) :
theorem WittVector.mapFun.nsmul {p : } {R : Type u_1} {S : Type u_2} [hp : Fact ()] [] [] (f : R →+* S) (n : ) (x : ) :
WittVector.mapFun (f) (n x) = n WittVector.mapFun (f) x
theorem WittVector.mapFun.zsmul {p : } {R : Type u_1} {S : Type u_2} [hp : Fact ()] [] [] (f : R →+* S) (z : ) (x : ) :
WittVector.mapFun (f) (z x) = z WittVector.mapFun (f) x
theorem WittVector.mapFun.pow {p : } {R : Type u_1} {S : Type u_2} [hp : Fact ()] [] [] (f : R →+* S) (x : ) (n : ) :
WittVector.mapFun (f) (x ^ n) = WittVector.mapFun (f) x ^ n
theorem WittVector.mapFun.natCast {p : } {R : Type u_1} {S : Type u_2} [hp : Fact ()] [] [] (f : R →+* S) (n : ) :
= n
@[deprecated WittVector.mapFun.natCast]
theorem WittVector.mapFun.nat_cast {p : } {R : Type u_1} {S : Type u_2} [hp : Fact ()] [] [] (f : R →+* S) (n : ) :
= n

Alias of WittVector.mapFun.natCast.

theorem WittVector.mapFun.intCast {p : } {R : Type u_1} {S : Type u_2} [hp : Fact ()] [] [] (f : R →+* S) (n : ) :
= n
@[deprecated WittVector.mapFun.intCast]
theorem WittVector.mapFun.int_cast {p : } {R : Type u_1} {S : Type u_2} [hp : Fact ()] [] [] (f : R →+* S) (n : ) :
= n

Alias of WittVector.mapFun.intCast.

An auxiliary tactic for proving that ghostFun respects the ring operations.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem WittVector.matrix_vecEmpty_coeff {p : } {R : Type u_6} (i : Fin 0) (j : ) :
(![] i).coeff j = ![] i j
@[deprecated _private.Mathlib.RingTheory.WittVector.Basic.0.WittVector.ghostFun_natCast]
theorem WittVector.ghostFun_nat_cast {p : } {R : Type u_1} [hp : Fact ()] [] (i : ) :
= i

Alias of _private.Mathlib.RingTheory.WittVector.Basic.0.WittVector.ghostFun_natCast.

@[deprecated _private.Mathlib.RingTheory.WittVector.Basic.0.WittVector.ghostFun_intCast]
theorem WittVector.ghostFun_int_cast {p : } {R : Type u_1} [hp : Fact ()] [] (i : ) :
= i

Alias of _private.Mathlib.RingTheory.WittVector.Basic.0.WittVector.ghostFun_intCast.

instance WittVector.instCommRing (p : ) (R : Type u_1) [hp : Fact ()] [] :

The commutative ring structure on 𝕎 R.

Equations
noncomputable def WittVector.map {p : } {R : Type u_1} {S : Type u_2} [hp : Fact ()] [] [] (f : R →+* S) :

WittVector.map f is the ring homomorphism 𝕎 R →+* 𝕎 S naturally induced by a ring homomorphism f : R →+* S. It acts coefficientwise.

Equations
• = { toFun := , map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
theorem WittVector.map_injective {p : } {R : Type u_1} {S : Type u_2} [hp : Fact ()] [] [] (f : R →+* S) (hf : ) :
theorem WittVector.map_surjective {p : } {R : Type u_1} {S : Type u_2} [hp : Fact ()] [] [] (f : R →+* S) (hf : ) :
@[simp]
theorem WittVector.map_coeff {p : } {R : Type u_1} {S : Type u_2} [hp : Fact ()] [] [] (f : R →+* S) (x : ) (n : ) :
(() x).coeff n = f (x.coeff n)
def WittVector.ghostMap {p : } {R : Type u_1} [hp : Fact ()] [] :
→+* R

WittVector.ghostMap is a ring homomorphism that maps each Witt vector to the sequence of its ghost components.

Equations
• WittVector.ghostMap = { toFun := WittVector.ghostFun, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
def WittVector.ghostComponent {p : } {R : Type u_1} [hp : Fact ()] [] (n : ) :

Evaluates the nth Witt polynomial on the first n coefficients of x, producing a value in R.

Equations
Instances For
theorem WittVector.ghostComponent_apply {p : } {R : Type u_1} [hp : Fact ()] [] (n : ) (x : ) :
= (MvPolynomial.aeval x.coeff) ()
@[simp]
theorem WittVector.ghostMap_apply {p : } {R : Type u_1} [hp : Fact ()] [] (x : ) (n : ) :
WittVector.ghostMap x n =
def WittVector.ghostEquiv (p : ) (R : Type u_1) [hp : Fact ()] [] [] :
≃+* (R)

WittVector.ghostMap is a ring isomorphism when p is invertible in R.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem WittVector.ghostEquiv_coe (p : ) (R : Type u_1) [hp : Fact ()] [] [] :
() = WittVector.ghostMap
theorem WittVector.ghostMap.bijective_of_invertible (p : ) (R : Type u_1) [hp : Fact ()] [] [] :
Function.Bijective WittVector.ghostMap
@[simp]
theorem WittVector.constantCoeff_apply {p : } {R : Type u_1} [hp : Fact ()] [] (x : ) :
WittVector.constantCoeff x = x.coeff 0
noncomputable def WittVector.constantCoeff {p : } {R : Type u_1} [hp : Fact ()] [] :

WittVector.coeff x 0 as a RingHom

Equations
• WittVector.constantCoeff = { toFun := fun (x : ) => x.coeff 0, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
instance WittVector.instNontrivial {p : } {R : Type u_1} [hp : Fact ()] [] [] :
Equations
• =