← All papers
Towards Solid Abelian Groups: A Formal Proof of Nöbeling's Theorem
math.LO
Sep 13, 2023 · v2
TL;DR
Formalizes Nöbeling's theorem in Lean using ordinal induction for condensed mathematics.
Abstract
Condensed mathematics, developed by Clausen and Scholze over the last few years, is a new way of studying the interplay between algebra and geometry. It replaces the concept of a topological space by a more sophisticated but better-behaved idea, namely that of a condensed set. Central to the theory are solid abelian groups and liquid vector spaces, analogues of complete topological groups. Nöbeling's theorem, concerning the structure of the abelian group of continuous maps from a profinite space to the integers, is a crucial ingredient in the theory of solid abelian groups; without it one cannot give any nonzero examples of solid abelian groups. This paper discusses a completed formalization of this result in the Lean theorem prover and provides a more detailed proof than previously available. The proof is somewhat unusual in that it requires induction over ordinals -- a technique which has not previously been used to a great extent in formalised mathematics.
Problem
Nobeling's theorem, which characterizes the structure of abelian groups of continuous maps from profinite spaces to the integers, is a crucial ingredient in the theory of solid abelian groups in condensed mathematics but had not been formally verified.
Approach
The authors formalize Nobeling's theorem in the Lean theorem prover. The proof requires induction over ordinals, a technique not previously used extensively in formalized mathematics. The formalization provides a more detailed proof than previously available in the literature.
Results
A complete formalization of Nobeling's theorem is achieved in Lean, providing a foundation for future formalization of solid abelian groups in condensed mathematics.