Papers With

← All papers
First page of Formalizing Norm Extensions and Applications to Number Theory

Formalizing Norm Extensions and Applications to Number Theory

María Inés de Frutos-Fernández

cs.LO Jun 29, 2023 · v1
formalization number-theory algebra mathlib
Read PDF arXiv abstract
TL;DR
Formalizes p-adic norm extensions and Fontaine period rings in Lean for number theory.
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 there is a unique norm on L extending the given norm on K, with an explicit description. As an application, the p-adic norm on Q_p is extended to its algebraic closure Q_p^alg, and the field C_p of p-adic complex numbers is defined as the completion of the latter. Building on C_p, we formalize the Fontaine period ring B_HT and discuss applications to Galois representations and p-adic Hodge theory. The formalized results are a prerequisite to formalize Local Class Field Theory, which is a fundamental ingredient of the proof of Fermat's Last Theorem.
Problem

Extending nonarchimedean norms from complete fields to algebraic extensions and constructing the p-adic complex numbers C_p requires careful formalization as a prerequisite for Local Class Field Theory and ultimately Fermat Last Theorem.

Approach

The authors formalize in Lean 4 that for a field K complete with respect to a nonarchimedean norm and an algebraic extension L/K, there is a unique extending norm with an explicit description. They extend the p-adic norm on Q_p to its algebraic closure, define C_p as the completion, and formalize the Fontaine period ring B_HT with applications to Galois representations and p-adic Hodge theory.

Results

The formalization provides machine-checked proofs of norm extension uniqueness and the construction of C_p and B_HT, establishing prerequisites for formalizing Local Class Field Theory in Lean.