Condensed Objects #

This file defines the category of condensed objects in a category C, following the work of Clausen-Scholze and Barwick-Haine.

Implementation Details #

We use the coherent Grothendieck topology on CompHaus, and define condensed objects in C to be C-valued sheaves, with respect to this Grothendieck topology.

In future work, we will define similar Grothendieck topologies on the category of profinite sets and extremally disconnected sets, and show that the three categories are equivalent (under suitable assumptions on C).

Note: Our definition more closely resembles "Pyknotic objects" in the sense of Barwick-Haine, as we do not impose cardinality bounds, and manage universes carefully instead.

References #

def Condensed (C : Type w) [CategoryTheory.Category.{v, w} C] :
Type (max (max (max (u + 1) w) u) v)

Condensed.{u} C is the category of condensed objects in a category C, which are defined as sheaves on CompHaus.{u} with respect to the coherent Grothendieck topology.

Instances For