Papers › Formalizing Norm Extensions and Applications to Number Theory
Formalizing Norm Extensions and Applications to Number Theory
María Inés de Frutos-Fernández
The archive published only this paper's code-link row. Authors, date and abstract are from arXiv's metadata (CC0), read from the Kaggle arXiv metadata snapshot of 2026-09-12 where its title matched the archive's; the title is the archive's.
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 ℚₚ of p-adic numbers to its algebraic closure ℚₚᵃˡᵍ, and we define the field ℂₚ of p-adic complex numbers as the completion of the latter with respect to the p-adic norm. Building on the definition of ℂₚ, we formalize the definition of the Fontaine period ring B_(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.
Code
Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Results from the paper archive 2025-07-28
No leaderboard rows for this paper in the archive.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections