Witt向量环的形式化
Formalizing the Ring of Witt Vectors
摘要：
基环$R$上的Witt向量环$\mathbb{W} R$是代数数论中的一个重要工具，是现代$p$ -adic Hodge理论的基础. $\mathbb{W} R$有一个有趣的性质，它从一个特征$p > 1$的环中构造出一个特征$0$的环，并且它可以更具体地用于从包含$\mathbb{Z}/p\mathbb{Z}$的有限域中构造$p$数$\mathbb{Q}_p$的相应的非分歧域扩张（直到同构为止是唯一的）。我们在精益证明助手中形式化了Witt向量的概念，以及相应的环运算和其他代数结构。我们证明了在精益，对于总理$p$，环的维特向量在$\mathbb{Z}/p\mathbb{Z}$是同构的环的$p$ -进整数$\mathbb{Z}_p$。在这个过程中，我们开发了一些习惯用法来干净地处理维特向量环上操作之间的恒等式计算。这些计算是棘手的一个天真的方法，并需要一个证明技术，通常是在非正式文献中略读。我们的证明类似于非正式的论点，而充分严格。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
