A Formalization of Complete Discrete Valuation Rings and Local Fields

TL;DR

This paper formalizes the theory of discretely valued fields and local fields in Lean, proving key properties and applications to number theory, including formal proofs that certain field extensions are local fields.

Contribution

It provides a formalized, rigorous foundation for the theory of local fields and discrete valuation rings within the Lean proof assistant, including new proofs of fundamental properties.

Findings

Unit ball with respect to a discrete valuation is a DVR

Adic valuation on a field of fractions is discrete

Finite extensions of _p and Laurent series fields are local fields

Abstract

Local fields, and fields complete with respect to a discrete valuation, are essential objects in commutative algebra, with applications to number theory and algebraic geometry. We formalize in Lean the basic theory of discretely valued fields. In particular, we prove that the unit ball with respect to a discrete valuation on a field is a discrete valuation ring and, conversely, that the adic valuation on the field of fractions of a discrete valuation ring is discrete. We define finite extensions of valuations and of discrete valuation rings, and prove some global-to-local results. Building on this general theory, we formalize the abstract definition and some fundamental properties of local fields. As an application, we show that finite extensions of the field $\mathbb{Q}_p$ of $p$-adic numbers and of the field $\mathbb{F}_p(\!(X)\!)$ of Laurent series over $\mathbb{F}_p$ are local fields.