Categorical Foundations of Formalized Condensed Mathematics

Autor:	Asgeirsson, Dagur, Brasca, Riccardo, Kuhn, Nikolas, di Capriglio, Filippo Alberto Edoardo Nuccio Mortarino Majno, Topaz, Adam
Rok vydání:	2024
Předmět:	Mathematics - Category Theory Computer Science - Formal Languages and Automata Theory Computer Science - Logic in Computer Science
Druh dokumentu:	Working Paper
Popis:	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. Comment: The Journal of Symbolic Logic, In press
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2407.12840 Zobrazit plný text záznamu View this record from Arxiv