Formalizing Norm Extensions and Applications to Number Theory

TL;DR

This paper formalizes the extension of norms in algebraic field extensions, applies this to $p$-adic fields, and discusses implications for $p$-adic Hodge theory and local class field theory.

Contribution

It provides a rigorous formalization of norm extensions and applies this to $p$-adic number fields and Galois representations, advancing the foundations of $p$-adic Hodge theory.

Findings

Unique norm extension on algebraic field extensions established

Construction of $p$-adic complex numbers $ ext{C}_p$ formalized

Framework for formalizing local class field theory developed

Abstract

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.