The paper describes a formalization in the
Lean proof assistant
in which we construct the ring of Witt vectors over a base ring
along with some of its important operations,
and show that the ring of Witt vectors over the integers modulo
is isomorphic to the ring of
Our project is incorporated into Lean’s mathematical library mathlib in the src/ring_theory/witt_vector directory. The mathlib project is constantly changing, and the files may have been updated since this paper was written. We preserve a branch of mathlib frozen on December 23, 2020, around the time that the corresponding paper was finalized and submitted to arXiv.
The code is written and tested with the community fork of Lean 3. To install it, please see https://leanprover-community.github.io/get_started.html.
We STRONGLY recommend following these directions, which will install elan, the Lean version manager, which will choose the correct version of Lean automatically.
The code is available as a branch of mathlib on github.
By following the installation instructions above,
a tool called
leanproject should have been installed.
leanproject get mathlib this branch will automatically be cloned
and precompiled binary artifacts will be downloaded from the cloud.
If you prefer to download the branch frozen at submission time,
leanproject get mathlib:witt-vectors-arxiv.
If you inspect the files in VSCode, you must use VSCode’s
Open Folder option
to open the project root directory.
You CANNOT open a single file (e.g. by double clicking on it) and browse interactively.
Easy way: from the command line, in the directory containing this file, type
and everything should work.
Our main contributions can be found in:
Other small contributions are scattered throughout the library, and are harder to point at.
We will now explain how these files correspond to the different subsections of the paper.
Section 3, and in particular Section 3.2 corresponds to the file
The material in 3.1 was added to
src/data/padics/padic_integers.lean, files that existed before this project began.
witt_simptactic appears in
is_poly.lean. Tactic definitions are identified by the keyword
witt_polynomial | structure_polynomial | defs | basic | is_poly |----------|-------------|------|----------| frobenius verschiebung mul_p init_tail teichmuller |----------|-------------| | identities truncated |--------------------| compare