Document Open Access Logo

Towards Solid Abelian Groups: A Formal Proof of Nöbeling’s Theorem

Author Dagur Asgeirsson

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2024.6.pdf
  • Filesize: 0.71 MB
  • 17 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • General and reference → Verification
  • Computing methodologies → Representation of mathematical objects
  • Mathematics of computing → Mathematical software
Keywords
  • Condensed mathematics
  • Nöbeling’s theorem
  • Lean
  • Mathlib
  • Interactive theorem proving

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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, a surprising result from the 1960s about 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. We discuss a recently completed formalisation of this result in the Lean theorem prover, and give a more detailed proof than those previously available in the literature. 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.

Cite As Get BibTex

Dagur Asgeirsson. Towards Solid Abelian Groups: A Formal Proof of Nöbeling’s Theorem. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.ITP.2024.6

Author Details

Dagur Asgeirsson
  • University of Copenhagen, Denmark

Funding

  • Asgeirsson, Dagur: The author was supported by the Danish National Research Foundation (DNRF) through the "Copenhagen Center for Geometry and Topology" under grant no. DNRF151.

Acknowledgements

First and foremost, I would like to thank Johan Commelin for encouraging me to start seriously working on this project when we were both in Banff attending the workshop on formalisation of cohomology theories last year. I had useful discussions related to this work with Johan, Kevin Buzzard, Adam Topaz, and Dustin Clausen. I am indebted to all four of them for providing helpful feedback on earlier drafts of this paper. Any project formalising serious mathematics in Lean depends on Mathlib, and this one is no exception. I am grateful to the Lean community as a whole for building and maintaining such a useful mathematical library, as well as providing an excellent forum for Lean-related discussions through the Zulip chat. Finally, I would like to thank the anonymous referees for helpful feedback.

Supplementary Materials

References

  1. Dagur Asgeirsson. Formalising discrete condensed sets. https://github.com/dagurtomas/lean-solid/tree/discrete, 2023.
  2. Dagur Asgeirsson. Formalising solid abelian groups. https://github.com/dagurtomas/lean-solid/, 2023.
  3. Clark Barwick and Peter Haine. Pyknotic objects, i. basic notions, 2019. URL: https://arxiv.org/abs/1904.09966.
  4. Alex J. Best, Christopher Birkbeck, Riccardo Brasca, and Eric Rodriguez Boidi. Fermat’s Last Theorem for Regular Primes. In Adam Naumowicz and René Thiemann, editors, 14th International Conference on Interactive Theorem Proving (ITP 2023), volume 268 of Leibniz International Proceedings in Informatics (LIPIcs), pages 36:1-36:8, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2023.36.
  5. Dustin Clausen and Peter Scholze. Condensed mathematics and complex geometry. https://people.mpim-bonn.mpg.de/scholze/Complex.pdf, 2022.
  6. Johan Commelin, Adam Topaz et al. Liquid tensor experiment. https://github.com/leanprover-community/lean-liquid, 2022.
  7. László Fuchs. Infinite Abelian Groups. ISSN. Elsevier Science, 1970. Google Scholar
  8. Andrew M. Gleason. Projective topological spaces. Illinois Journal of Mathematics, 2(4A):482-489, 1958. URL: https://doi.org/10.1215/ijm/1255454110.
  9. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A machine-checked proof of the odd order theorem. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving, pages 163-179, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  10. The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367-381, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373824.
  11. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25, pages 378-388, Cham, 2015. Springer International Publishing. Google Scholar
  12. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28, pages 625-635, Cham, 2021. Springer International Publishing. Google Scholar
  13. Oliver Nash. A Formalisation of Gallagher’s Ergodic Theorem. In Adam Naumowicz and René Thiemann, editors, 14th International Conference on Interactive Theorem Proving (ITP 2023), volume 268 of Leibniz International Proceedings in Informatics (LIPIcs), pages 23:1-23:16, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2023.23.
  14. Georg Nöbeling. Verallgemeinerung eines Satzes von Herrn E. Specker. Invent. Math., 6:41-55, 1968. URL: https://doi.org/10.1007/BF01389832.
  15. Peter Scholze. Lectures on analytic geometry. http://www.math.uni-bonn.de/people/scholze/Analytic.pdf, 2019.
  16. Peter Scholze. Lectures on condensed mathematics. https://www.math.uni-bonn.de/people/scholze/Condensed.pdf, 2019.
  17. Peter Scholze. Liquid tensor experiment. Experimental Mathematics, 31(2):349-354, 2022. URL: https://doi.org/10.1080/10586458.2021.1926016.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact