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

• Commelin and Lewis, Formalizing the Ring of Witt Vectors

def WittVector.mapFun {p : Nat} {α : 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

• Eq (WittVector.mapFun f x) (WittVector.mk p (Function.comp f x.coeff))

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

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

def WittVector.mapFun.tacticMap_fun_tac : Lean.ParserDescr

Auxiliary tactic for showing that mapFun respects the ring operations.

Equations

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

theorem WittVector.mapFun.zero {p : Nat} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (f : RingHom R S) : Eq (mapFun (DFunLike.coe f) 0) 0

theorem WittVector.mapFun.one {p : Nat} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (f : RingHom R S) : Eq (mapFun (DFunLike.coe f) 1) 1

theorem WittVector.mapFun.add {p : Nat} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (f : RingHom R S) (x y : WittVector p R) : Eq (mapFun (DFunLike.coe f) (HAdd.hAdd x y)) (HAdd.hAdd (mapFun (DFunLike.coe f) x) (mapFun (DFunLike.coe f) y))

theorem WittVector.mapFun.sub {p : Nat} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (f : RingHom R S) (x y : WittVector p R) : Eq (mapFun (DFunLike.coe f) (HSub.hSub x y)) (HSub.hSub (mapFun (DFunLike.coe f) x) (mapFun (DFunLike.coe f) y))

theorem WittVector.mapFun.mul {p : Nat} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (f : RingHom R S) (x y : WittVector p R) : Eq (mapFun (DFunLike.coe f) (HMul.hMul x y)) (HMul.hMul (mapFun (DFunLike.coe f) x) (mapFun (DFunLike.coe f) y))

theorem WittVector.mapFun.neg {p : Nat} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (f : RingHom R S) (x : WittVector p R) : Eq (mapFun (DFunLike.coe f) (Neg.neg x)) (Neg.neg (mapFun (DFunLike.coe f) x))

theorem WittVector.mapFun.nsmul {p : Nat} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (f : RingHom R S) (n : Nat) (x : WittVector p R) : Eq (mapFun (DFunLike.coe f) (HSMul.hSMul n x)) (HSMul.hSMul n (mapFun (DFunLike.coe f) x))

theorem WittVector.mapFun.zsmul {p : Nat} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (f : RingHom R S) (z : Int) (x : WittVector p R) : Eq (mapFun (DFunLike.coe f) (HSMul.hSMul z x)) (HSMul.hSMul z (mapFun (DFunLike.coe f) x))

theorem WittVector.mapFun.pow {p : Nat} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (f : RingHom R S) (x : WittVector p R) (n : Nat) : Eq (mapFun (DFunLike.coe f) (HPow.hPow x n)) (HPow.hPow (mapFun (DFunLike.coe f) x) n)

theorem WittVector.mapFun.natCast {p : Nat} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (f : RingHom R S) (n : Nat) : Eq (mapFun (DFunLike.coe f) n.cast) n.cast

theorem WittVector.mapFun.intCast {p : Nat} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (f : RingHom R S) (n : Int) : Eq (mapFun (DFunLike.coe f) n.cast) n.cast

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 : Nat} {R : Type u_5} (i : Fin 0) (j : Nat) : Eq ((Matrix.vecEmpty i).coeff j) (Matrix.vecEmpty i j)

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

The commutative ring structure on 𝕎 R.

Equations

• Eq (WittVector.instCommRing p R) (Function.Surjective.commRing (WittVector.mapFun (DFunLike.coe (MvPolynomial.counit R))) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯)

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

• Eq (WittVector.map f) { toFun := WittVector.mapFun (DFunLike.coe f), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem WittVector.map_injective {p : Nat} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (f : RingHom R S) (hf : Function.Injective (DFunLike.coe f)) : Function.Injective (DFunLike.coe (map f))

theorem WittVector.map_surjective {p : Nat} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (f : RingHom R S) (hf : Function.Surjective (DFunLike.coe f)) : Function.Surjective (DFunLike.coe (map f))

theorem WittVector.map_coeff {p : Nat} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] (f : RingHom R S) (x : WittVector p R) (n : Nat) : Eq ((DFunLike.coe (map f) x).coeff n) (DFunLike.coe f (x.coeff n))

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

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

Equations

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

def WittVector.ghostComponent {p : Nat} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (n : Nat) : RingHom (WittVector p R) R

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

Equations

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

theorem WittVector.ghostComponent_apply {p : Nat} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (n : Nat) (x : WittVector p R) : Eq (DFunLike.coe (ghostComponent n) x) (DFunLike.coe (MvPolynomial.aeval x.coeff) (wittPolynomial p Int n))

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

def WittVector.ghostEquiv (p : Nat) (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] [Invertible p.cast] : RingEquiv (WittVector p R) (Nat → R)

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

Equations

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

theorem WittVector.ghostEquiv_coe (p : Nat) (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] [Invertible p.cast] : Eq (RingHomClass.toRingHom (ghostEquiv p R)) ghostMap

theorem WittVector.ghostMap.bijective_of_invertible (p : Nat) (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] [Invertible p.cast] : Function.Bijective (DFunLike.coe ghostMap)

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

WittVector.coeff x 0 as a RingHom

Equations

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

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

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