Formalizing Norm Extensions and Applications to Number Theory
| Autor: | de Frutos-Fernández, María Inés |
|---|---|
| Rok vydání: | 2023 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | Let $K$ be a field complete with respect to a nonarchimedean real-valued norm, and let $L/K$ be an algebraic extension. We show that there is a unique norm on $L$ extending the given norm on $K$, with an explicit description. As an application, we extend the $p$-adic norm on the field $\mathbb{Q}_p$ of $p$-adic numbers to its algebraic closure $\mathbb{Q}_p^{\text{alg}}$, and we define the field $\mathbb{C}_p$ of $p$-adic complex numbers as the completion of the latter with respect to the $p$-adic norm. Building on the definition of $\mathbb{C}_p$, we formalize the definition of the Fontaine period ring $B_{\text{HT}}$ and discuss some applications to the theory of Galois representations and to $p$-adic Hodge theory. The results formalized in this paper are a prerequisite to formalize Local Class Field Theory, which is a fundamental ingredient of the proof of Fermat's Last Theorem. Comment: Accepted for the 14th International Conference on Interactive Theorem Proving (ITP 2023). 18 pages |
| Databáze: | arXiv |
| Externí odkaz: |
|