Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A formal characterization of discrete condensed objects

Dagur Asgeirsson

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.

A formal characterization of discrete condensed objects

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.

Paper Structure

This paper contains 24 sections, 32 theorems, 68 equations.

Table of Contents

  1. Introduction
  2. Main results
  3. Application
  4. Terminology and notation
  5. Outline
  6. Preliminaries
  7. Generalities in category theory
  8. Adjunctions
  9. Initial and final functors
  10. Set-theoretic issues in condensed mathematics
  11. Sheafification in mathlib
  12. Constant sheaves
  13. The functors from $\mathsf{Set}$ to $\mathsf{CondSet}$
  14. Naturality of the counit
  15. Triangle identities
  16. ...and 9 more sections

Key Result

Theorem A

https://github.com/leanprover-community/mathlib4/blob/ffb2f0dbf80ad18fa75f85bd0facee6737b59acf/Mathlib/Condensed/Discrete/Characterization.lean#L74-L104 A condensed set is discrete if and only if it is in the essential image of the functor i.e. if there exists some set $X'$ and an isomorphism of condensed sets

Theorems & Definitions (64)

  • Definition 1.1
  • Theorem A
  • Theorem B
  • Theorem C
  • Proposition 2.1
  • proof
  • Proposition 2.2
  • proof
  • Corollary 2.3
  • Definition 2.4
  • ...and 54 more