论文标题
正式化Witt向量的戒指
Formalizing the Ring of Witt Vectors
论文作者
论文摘要
基本环$ r $上的witt vectors $ \ mathbb {w} r $是代数数理论中的重要工具，是现代$ p $ addic hodge理论的基础。 $ \ Mathbb {w} r $具有有趣的属性，它构建了特征性的$ 0 $ $ 0 $ $ p> 1 $，并且可以更具体地从包含$ \ mathbb {z}/p \ m \ mathbb {z}的有限字段构造是独一无二的同构）。 我们在精益证明助手中正式将Witt向量的概念以及相应的环操作和其他代数结构形式化。我们证明，对于Prime $ p $，$ \ mathbb {z}/p \ mathbb {z} $上的witt vector的戒指对$ p $ - adic integers $ \ mathbb {z} _p $的戒指是同构的。在此过程中，我们开发成语，以清晰处理Witt向量环上操作之间身份的计算。这些计算以幼稚的方法很棘手，并且需要一种通常在非正式文献中掠过的证明技术。我们的证明类似于非正式论点，同时完全严格。
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.
