This page contains supplementary material for the paper Formalizing the Ring of Witt Vectors (arXiv) by Johan Commelin and Robert Y. Lewis, published in the proceedings of CPP ‘21.
The paper describes a formalization in the
Lean proof assistant
in which we construct the ring of Witt vectors over a base ring R
along with some of its important operations,
and show that the ring of Witt vectors over the integers modulo p
is isomorphic to the ring of p
adic integers.
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://leanprovercommunity.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.
See https://github.com/leanprovercommunity/mathlib/tree/wittvectorsarxiv.
By following the installation instructions above,
a tool called leanproject
should have been installed.
By running 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,
run leanproject get mathlib:wittvectorsarxiv
.
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
code .
and everything should work.
Our main contributions can be found in:
src/data/padics/ring_homs.lean
src/ring_theory/witt_vector/
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 src/data/padics/ring_homs.lean
.
The material in 3.1 was added to src/ring_theory/discrete_valuation_ring.lean
and
src/data/padics/padic_integers.lean
, files that existed before this project began.
src/data/mv_polynomial/monad.lean
src/ring_theory/witt_vector/structure_polynomial.lean
,
src/ring_theory/witt_vector/witt_polynomial.lean
src/ring_theory/witt_vector/defs.lean
src/ring_theory/witt_vector/is_poly.lean
src/ring_theory/witt_vector/basic.lean
basic.lean
.
The witt_simp
tactic appears in is_poly.lean
.
Tactic definitions are identified by the keyword meta def
.src/ring_theory/witt_vector/
, frobenius.lean
, verschiebung.lean
, mul_p.lean
,
teichmuller.lean
, witt_sub.lean
, identities.lean
.src/ring_theory/witt_vector/truncated.lean
, src/ring_theory/witt_vector/compare.lean
witt_polynomial

structure_polynomial

defs

basic

is_poly

frobenius verschiebung mul_p init_tail teichmuller
 
identities truncated

compare