Formalizing Norm Extensions and Applications to Number Theory

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.