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 : α → β) : WittVector p α → WittVector p β

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

theorem WittVector.mapFun.injective {p : ℕ} {α : Type u_4} {β : Type u_5} (f : α → β) (hf : Function.Injective f) : Function.Injective (WittVector.mapFun f)

theorem WittVector.mapFun.surjective {p : ℕ} {α : Type u_4} {β : Type u_5} (f : α → β) (hf : Function.Surjective f) : Function.Surjective (WittVector.mapFun f)

def WittVector.mapFun.tacticMap_fun_tac : Lean.ParserDescr

Auxiliary tactic for showing that mapFun respects the ring operations.

theorem WittVector.mapFun.zero {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : Fact (Nat.Prime p)] [CommRing R] [CommRing S] (f : R →+* S) : WittVector.mapFun (↑f) 0 = 0

theorem WittVector.mapFun.one {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : Fact (Nat.Prime p)] [CommRing R] [CommRing S] (f : R →+* S) : WittVector.mapFun (↑f) 1 = 1

theorem WittVector.mapFun.add {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : Fact (Nat.Prime p)] [CommRing R] [CommRing S] (f : R →+* S) (x : WittVector p R) (y : WittVector p R) : 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 (Nat.Prime p)] [CommRing R] [CommRing S] (f : R →+* S) (x : WittVector p R) (y : WittVector p R) : 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 (Nat.Prime p)] [CommRing R] [CommRing S] (f : R →+* S) (x : WittVector p R) (y : WittVector p R) : 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 (Nat.Prime p)] [CommRing R] [CommRing S] (f : R →+* S) (x : WittVector p R) : WittVector.mapFun (↑f) (-x) = -WittVector.mapFun (↑f) x

theorem WittVector.mapFun.nsmul {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : Fact (Nat.Prime p)] [CommRing R] [CommRing S] (f : R →+* S) (x : WittVector p R) (n : ℕ) : 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 (Nat.Prime p)] [CommRing R] [CommRing S] (f : R →+* S) (x : WittVector p R) (z : ℤ) : 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 (Nat.Prime p)] [CommRing R] [CommRing S] (f : R →+* S) (x : WittVector p R) (n : ℕ) : WittVector.mapFun (↑f) (x ^ n) = WittVector.mapFun (↑f) x ^ n

theorem WittVector.mapFun.nat_cast {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : Fact (Nat.Prime p)] [CommRing R] [CommRing S] (f : R →+* S) (n : ℕ) : WittVector.mapFun ↑f ↑n = ↑n

theorem WittVector.mapFun.int_cast {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : Fact (Nat.Prime p)] [CommRing R] [CommRing S] (f : R →+* S) (n : ℤ) : WittVector.mapFun ↑f ↑n = ↑n

def WittVector.«tacticGhost_fun_tac_,_» : Lean.ParserDescr

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

theorem WittVector.matrix_vecEmpty_coeff {p : ℕ} {R : Type u_6} (i : Fin 0) (j : ℕ) : WittVector.coeff ![] j = ![]

instance WittVector.instCommRingWittVector (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] : CommRing (WittVector p R)

The commutative ring structure on 𝕎 R.

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

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

theorem WittVector.map_injective {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : Fact (Nat.Prime p)] [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Injective ↑f) : Function.Injective ↑(WittVector.map f)

theorem WittVector.map_surjective {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : Fact (Nat.Prime p)] [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ↑f) : Function.Surjective ↑(WittVector.map f)

@[simp]

theorem WittVector.map_coeff {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : Fact (Nat.Prime p)] [CommRing R] [CommRing S] (f : R →+* S) (x : WittVector p R) (n : ℕ) : WittVector.coeff (↑(WittVector.map f) x) n = ↑f (WittVector.coeff x n)

def WittVector.ghostMap {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] : WittVector p R →+* ℕ → R

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

def WittVector.ghostComponent {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (n : ℕ) : WittVector p R →+* R

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

theorem WittVector.ghostComponent_apply {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (n : ℕ) (x : WittVector p R) : ↑(WittVector.ghostComponent n) x = ↑(MvPolynomial.aeval x.coeff) (wittPolynomial p ℤ n)

@[simp]

theorem WittVector.ghostMap_apply {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x : WittVector p R) (n : ℕ) : ↑WittVector.ghostMap x n = ↑(WittVector.ghostComponent n) x

def WittVector.ghostEquiv (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] [Invertible ↑p] : WittVector p R ≃+* (ℕ → R)

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

@[simp]

theorem WittVector.ghostEquiv_coe (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] [Invertible ↑p] : ↑(WittVector.ghostEquiv p R) = WittVector.ghostMap

theorem WittVector.ghostMap.bijective_of_invertible (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] [Invertible ↑p] : Function.Bijective ↑WittVector.ghostMap

@[simp]

theorem WittVector.constantCoeff_apply {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x : WittVector p R) : ↑WittVector.constantCoeff x = WittVector.coeff x 0

noncomputable def WittVector.constantCoeff {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] : WittVector p R →+* R

WittVector.coeff x 0 as a RingHom

instance WittVector.instNontrivialWittVector {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] [Nontrivial R] : Nontrivial (WittVector p R)