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_3} {β : Type u_4} (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.

Equations

• WittVector.mapFun f x = WittVector.mk p (f ∘ x.coeff)

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

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

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

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

theorem WittVector.mapFun.add {p : ℕ} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (f : R →+* S) (x y : WittVector p R) : mapFun (⇑f) (x + y) = mapFun (⇑f) x + mapFun (⇑f) y

theorem WittVector.mapFun.sub {p : ℕ} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (f : R →+* S) (x y : WittVector p R) : mapFun (⇑f) (x - y) = mapFun (⇑f) x - mapFun (⇑f) y

theorem WittVector.mapFun.mul {p : ℕ} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (f : R →+* S) (x y : WittVector p R) : mapFun (⇑f) (x * y) = mapFun (⇑f) x * mapFun (⇑f) y

theorem WittVector.mapFun.neg {p : ℕ} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (f : R →+* S) (x : WittVector p R) : mapFun (⇑f) (-x) = -mapFun (⇑f) x

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

theorem WittVector.mapFun.zsmul {p : ℕ} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (f : R →+* S) (z : ℤ) (x : WittVector p R) : mapFun (⇑f) (z • x) = z • mapFun (⇑f) x

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

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

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

@[instance_reducible]

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

The commutative ring structure on 𝕎 R.

Equations

• WittVector.instCommRing p R = Function.Surjective.commRing (WittVector.mapFun ⇑(MvPolynomial.counit R)) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable def WittVector.map {p : ℕ} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (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.

Equations

• WittVector.map f = { toFun := WittVector.mapFun ⇑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

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

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

@[simp]

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

@[simp]

theorem WittVector.map_id {p : ℕ} (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] : map (RingHom.id R) = RingHom.id (WittVector p R)

theorem WittVector.map_eq_zero_iff {p : ℕ} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (f : R →+* S) {x : WittVector p R} : (map f) x = 0 ↔ ∀ (n : ℕ), f (x.coeff n) = 0

noncomputable def WittVector.ghostMap {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] : WittVector p R →+* ℕ → 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' := ⋯ }

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

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

Equations

• WittVector.ghostComponent n = (Pi.evalRingHom (fun (a : ℕ) => R) n).comp WittVector.ghostMap

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

theorem WittVector.pow_dvd_ghostComponent_of_dvd_coeff {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] {x : WittVector p R} {n : ℕ} (hx : ∀ i ≤ n, ↑p ∣ x.coeff i) : ↑p ^ (n + 1) ∣ (ghostComponent n) x

@[simp]

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

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

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

Equations

• WittVector.ghostEquiv p R = { toFun := (↑↑WittVector.ghostMap).toFun, invFun := (WittVector.ghostEquiv'✝ p R).invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

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

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

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

WittVector.coeff x 0 as a RingHom

Equations

• WittVector.constantCoeff = { toFun := fun (x : WittVector p R) => x.coeff 0, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

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

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