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.

Equations

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

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.

Equations

• WittVector.mapFun.tacticMap_fun_tac = Lean.ParserDescr.node `WittVector.mapFun.tacticMap_fun_tac 1024 (Lean.ParserDescr.nonReservedSymbol "map_fun_tac" false)

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) (n : ℕ) (x : WittVector p R) : 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) (z : ℤ) (x : WittVector p R) : 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.natCast {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.intCast {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.

Equations

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

theorem WittVector.matrix_vecEmpty_coeff {p : ℕ} {R : Type u_6} (i : Fin 0) (j : ℕ) : ![].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.

Equations

• WittVector.instCommRingWittVector p R = Function.Surjective.commRing (WittVector.mapFun ⇑(MvPolynomial.counit 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.

Equations

• WittVector.map f = { toMonoidHom := { toOneHom := { 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} [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.map f) x).coeff n = f (x.coeff 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.

Equations

• WittVector.ghostMap = { toMonoidHom := { toOneHom := { toFun := WittVector.ghostFun, map_one' := ⋯ }, map_mul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

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.

Equations

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

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.

Equations

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

@[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 = x.coeff 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

Equations

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

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

Equations

• ⋯ = ⋯