Categorical Foundations of Formalized Condensed Mathematics
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866915035078459392 |
|---|---|
| author | Asgeirsson, Dagur Brasca, Riccardo Kuhn, Nikolas di Capriglio, Filippo Alberto Edoardo Nuccio Mortarino Majno Topaz, Adam |
| author_facet | Asgeirsson, Dagur Brasca, Riccardo Kuhn, Nikolas di Capriglio, Filippo Alberto Edoardo Nuccio Mortarino Majno Topaz, Adam |
| 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 for the coherent topology on a certain category of compact Hausdorff spaces. In this case, the sheaf condition has a fairly simple explicit description, which arises from studying the relationship between the coherent, regular and extensive topologies. In this paper, we establish this relationship under minimal assumptions on the category, going beyond the case of compact Hausdorff spaces. Along the way, we also provide a characterization of sheaves and covering sieves for these categories. All results in this paper have been fully formalized in the Lean proof assistant. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_12840 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Categorical Foundations of Formalized Condensed Mathematics Asgeirsson, Dagur Brasca, Riccardo Kuhn, Nikolas di Capriglio, Filippo Alberto Edoardo Nuccio Mortarino Majno Topaz, Adam 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 for the coherent topology on a certain category of compact Hausdorff spaces. In this case, the sheaf condition has a fairly simple explicit description, which arises from studying the relationship between the coherent, regular and extensive topologies. In this paper, we establish this relationship under minimal assumptions on the category, going beyond the case of compact Hausdorff spaces. Along the way, we also provide a characterization of sheaves and covering sieves for these categories. All results in this paper have been fully formalized in the Lean proof assistant. |
| title | Categorical Foundations of Formalized Condensed Mathematics |
| topic | Category Theory Formal Languages and Automata Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2407.12840 |