← All papers
Formalizing the Ring of Witt Vectors
cs.LO
Oct 6, 2020 · v2
TL;DR
Formalizes Witt vectors and proves their isomorphism with p-adic integers in Lean.
Abstract
The ring of Witt vectors over a base ring R is an important tool in algebraic number theory and lies at the foundations of modern p-adic Hodge theory. It 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 Z/pZ the corresponding unramified field extension of the p-adic numbers. 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 Z/pZ is isomorphic to the ring of p-adic integers. 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.
Problem
The ring of Witt vectors, fundamental to algebraic number theory and p-adic Hodge theory, involves intricate algebraic identities that are typically hand-waved in informal presentations. No prior formalization existed.
Approach
The authors formalize Witt vectors in the Lean proof assistant, defining the ring operations and algebraic structure. They develop proof idioms for handling the combinatorially complex identities between Witt vector operations, which are intractable with naive approaches and usually glossed over in textbooks.
Results
The formalization proves that for prime p, the ring of Witt vectors over Z/pZ is isomorphic to the p-adic integers. The developed proof techniques handle calculations that informal sources typically skip.