A formal characterization of discrete condensed objects
Fuente:
arXiv
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866916458988044288 |
|---|---|
| author | Asgeirsson, Dagur |
| author_facet | Asgeirsson, Dagur |
| contents | Condensed mathematics, developed by Clausen and Scholze over the last few years, proposes a generalization of topology with better categorical properties. It replaces the concept of a topological space by that of a condensed set, which can be defined as a sheaf on a certain site of compact Hausdorff spaces. Since condensed sets are supposed to be a generalization of topological spaces, one would like to be able to study the notion of discreteness. There are various ways to define what it means for a condensed set to be discrete. In this paper we describe them, and prove that they are equivalent. The results have been fully formalized in the Lean proof assistant. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_17847 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A formal characterization of discrete condensed objects Asgeirsson, Dagur Category Theory Formal Languages and Automata Theory Logic in Computer Science Condensed mathematics, developed by Clausen and Scholze over the last few years, proposes a generalization of topology with better categorical properties. It replaces the concept of a topological space by that of a condensed set, which can be defined as a sheaf on a certain site of compact Hausdorff spaces. Since condensed sets are supposed to be a generalization of topological spaces, one would like to be able to study the notion of discreteness. There are various ways to define what it means for a condensed set to be discrete. In this paper we describe them, and prove that they are equivalent. The results have been fully formalized in the Lean proof assistant. |
| title | A formal characterization of discrete condensed objects |
| topic | Category Theory Formal Languages and Automata Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2410.17847 |