Formalizing the Ring of Witt Vectors

TL;DR

This paper formalizes the theory of Witt vectors in the Lean proof assistant, proving their isomorphism to p-adic integers and developing new proof techniques for algebraic identities.

Contribution

It introduces a formalization of Witt vectors in Lean, including their algebraic structure and key isomorphisms, with novel proof strategies for complex identities.

Findings

Witt vectors over Z/pZ are isomorphic to Z_p.

Developed new proof idioms for identities in Witt vectors.

Formalized algebraic operations of Witt vectors in Lean.

Abstract

The ring of Witt vectors $\mathbb{W} R$ over a base ring $R$ is an important tool in algebraic number theory and lies at the foundations of modern $p$-adic Hodge theory. $\mathbb{W} R$ has the interesting property that it constructs a ring of characteristic $0$ out of a ring of characteristic $p > 1$, and it can be used more specifically to construct from a finite field containing $\mathbb{Z}/p\mathbb{Z}$ the corresponding unramified field extension of the $p$-adic numbers $\mathbb{Q}_p$ (which is unique up to isomorphism). We formalize the notion of a Witt vector in the Lean proof assistant, along with the corresponding ring operations and other algebraic structure. We prove in Lean that, for prime $p$, the ring of Witt vectors over $\mathbb{Z}/p\mathbb{Z}$ is isomorphic to the ring of $p$-adic integers $\mathbb{Z}_p$. In the process we develop idioms to cleanly handle calculations of identities between operations on the ring of Witt vectors. These calculations are intractable with a naive approach, and require a proof technique that is usually skimmed over in the informal literature. Our proofs resemble the informal arguments while being fully rigorous.