Categorical Foundations of Formalized Condensed Mathematics

TL;DR

This paper develops the categorical foundations of condensed mathematics, extending the theory beyond compact Hausdorff spaces and formalizing the results in the Lean proof assistant.

Contribution

It generalizes the relationship between different topologies in condensed mathematics under minimal assumptions and characterizes sheaves and coverings in these categories.

Findings

Established the relationship between topologies beyond compact Hausdorff spaces.

Provided a characterization of sheaves and covering sieves for these categories.

Fully formalized all results in the Lean proof assistant.

Abstract

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.