A Formalization of Complete Discrete Valuation Rings and Local Fields
summary
Formalization uses 8,000 lines of Lean 3 and mathlib to encode discrete valuations, show the unit ball is a discrete valuation ring and conversely build the adic valuation on a fraction field, define and extend valuations to finite extensions with uniqueness and completeness, and prove the integral closure of the unit ball equals the unit ball of the extension. Constructions use a multiplicative-set set_mz representation; results include that finite extensions of Qp and Fp((X)) are local fields (code and paper linked).
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:12Motivation from number theory
- 6:31Local fields and p-adic numbers
- 9:05Abstract definition of local fields
- 10:08Discrete valuations
- 14:21Discrete valuation rings
- 18:54Formal definition of local fields
- 19:37Complete fields with discrete valuations
- 21:46Future work on class field theory
- 22:57Q&A
related talks
01h 08mAlgebraic Structures in Logic and Query Evaluation 4
01h 05mAlgebraic Structures in Logic and Query Evaluation 2
01h 06mSemiring Semantics
24mWhen Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
01h 02mAlgebraic Structures in Logic and Query Evaluation 3
22mFormalization of a Proof Calculus for Incremental Linearization for Satisfiability(…)
19mRamsey Quantifiers in Linear Arithmetics
01h 06mAlgebraic Structures in Logic and Query Evaluation 1