Papers With

← All papers
First page of A Formalization of Complete Discrete Valuation Rings and Local Fields

A Formalization of Complete Discrete Valuation Rings and Local Fields

María Inés de Frutos-Fernández, Filippo A. E. Nuccio Mortarino Majno di Capriglio

cs.LO Oct 3, 2023 · v2
formalization mathlib number-theory algebra
Read PDF arXiv abstract
TL;DR
Formalizes discrete valuation rings and local fields in Lean with contributions to mathlib.
Abstract
We formalize in Lean the basic theory of discretely valued fields. 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 DVR is discrete. We define finite extensions of valuations and discrete valuation rings, proving global-to-local results. Building on this, we formalize the abstract definition and fundamental properties of local fields, showing that finite extensions of the p-adic numbers and the Laurent series field over a finite field are local fields.
Problem

The theory of discretely valued fields and local fields is fundamental in algebraic number theory, but had not been formalized in Lean. Definitions and basic properties of local fields, DVRs, and their extensions were missing from the formal library.

Approach

The authors formalize in Lean the basic theory of discretely valued fields: proving that the unit ball of a discrete valuation is a DVR and conversely that the adic valuation on the fraction field of a DVR is discrete. They define finite extensions of valuations and DVRs, proving global-to-local results, and formalize the abstract definition of local fields.

Results

The formalization shows that finite extensions of the p-adic numbers and the Laurent series field over a finite field are local fields. Global-to-local results for extensions of DVRs are proved formally, providing foundational infrastructure for algebraic number theory in Lean.