Formalizing the Ring of Witt Vectors

DOI10.1145/3437992.3439919MaRDI QIDQ6350627zbMATH OpenFDO

Authors Johan Commelin, Robert Y. Lewis

Publication date 6 October 2020

Full work available at URL https://doi.org/10.1145/3437992.3439919

Abstract: The ring of Witt vectors $mathbbWR$ over a base ring $R$ is an important tool in algebraic number theory and lies at the foundations of modern $p$-adic Hodge theory. $mathbbWR$ 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 $mathbbZ/pmathbbZ$ 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 $mathbbZ/pmathbbZ$ 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.

This page was built for publication: Formalizing the Ring of Witt Vectors

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6350627)