A formal characterization of discrete condensed objects

TL;DR

This paper provides a formal, equivalent characterization of discrete objects within condensed mathematics, enhancing understanding of their properties and formal verification using the Lean proof assistant.

Contribution

It offers a comprehensive, formal analysis of discrete condensed objects and proves the equivalence of various definitions within this framework.

Findings

Multiple definitions of discreteness are shown to be equivalent.

The formalization in Lean ensures rigorous verification of the results.

The work advances the foundational understanding of condensed sets.

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 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.