Towards solid abelian groups: A formal proof of Nöbeling's theorem
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910661724864512 |
|---|---|
| author | Asgeirsson, Dagur |
| author_facet | Asgeirsson, Dagur |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2309_07252 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Towards solid abelian groups: A formal proof of Nöbeling's theorem Asgeirsson, Dagur Logic Logic in Computer Science General Topology 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. |
| title | Towards solid abelian groups: A formal proof of Nöbeling's theorem |
| topic | Logic Logic in Computer Science General Topology |
| url | https://arxiv.org/abs/2309.07252 |