Formalizing Norm Extensions and Applications to Number Theory

Non-Archimedean valued fields (12J25) Non-Archimedean analysis (26E30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

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

m a t h b b Q_{p}

of

p

-adic numbers to its algebraic closure

m a t h b b Q_{p}^{e x t a l g}

, and we define the field

m a t h b b 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

m a t h b b C_{p}

, we formalize the definition of the Fontaine period ring

B_{e x t H T}

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.

This page was built for publication: Formalizing Norm Extensions and Applications to Number Theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6442034)