Formalizing Norm Extensions and Applications to Number Theory

Maria Ines de Frutos Fernandez
Imperial College London

Let K be a eld complete with respect to a nonarchimedean real-valued
norm, and let L=K be an algebraic extension. We formalize in Lean 3 the
proof that there is a unique norm on L extending the given norm on K, and
we provide an explicit description of this norm. This is a prerequisite to
formalize Local Class Field Theory, which is an essential component in the
proof of Fermat's Last Theorem.
As an application, we extend the p-adic norm on the eld Qp of p-adic
numbers to its algebraic closure Qalg
p , and we de ne the eld Cp, a p-adic
analogue of the complex numbers.
Building on the de nition of Cp, we formalize the de nition of the
Fontaine period ring BHT. Both Cp and BHT can be used to detect cer-
tain properties of Galois representations.

1Imperial College London / Universidad Autonoma de Madrid

Presentation (PDF File)

Back to Machine Assisted Proofs