Papers With

← All papers
First page of Categorical Foundations of Formalized Condensed Mathematics

Categorical Foundations of Formalized Condensed Mathematics

Dagur Asgeirsson, Riccardo Brasca, Nikolas Kuhn, Filippo A. E. Nuccio Mortarino Majno di Capriglio, Adam Topaz

math.CT Jul 4, 2024 · v2
formalization category-theory topology mathlib
Read PDF arXiv abstract
TL;DR
Fully formalizes categorical foundations for condensed mathematics in Lean.
Abstract
Condensed mathematics, developed by Clausen and Scholze, proposes a generalization of topology with improved categorical properties. It replaces topological spaces with condensed sets, defined as sheaves for the coherent topology on a certain category of compact Hausdorff spaces. The sheaf condition has a simple explicit description arising from studying the relationship between the coherent, regular and extensive topologies. We establish this relationship under minimal assumptions on the category, going beyond the case of compact Hausdorff spaces, while also providing a characterization of sheaves and covering sieves for these categories. All results are fully formalized in the Lean proof assistant.
Problem

Condensed mathematics, developed by Clausen and Scholze, generalizes topology with better categorical properties by replacing topological spaces with sheaves on compact Hausdorff spaces. Formalizing the sheaf condition and its relationship to coherent, regular, and extensive topologies requires establishing these connections under minimal categorical assumptions.

Approach

The authors establish the relationship between coherent, regular, and extensive topologies under minimal assumptions on the category, going beyond compact Hausdorff spaces. They provide a characterization of sheaves using explicit conditions arising from this relationship. The work is formalized in Lean as part of the Mathlib library's condensed mathematics development.

Results

The formalization provides categorical foundations for condensed mathematics in Lean/Mathlib, establishing the sheaf-condition equivalences under general assumptions and contributing infrastructure for further formalized development of condensed mathematics.