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

• [barwickhaine2019]: Pyknotic objects, I. Basic notions, 2019.
• [scholze2019condensed]: Lectures on Condensed Mathematics, 2019.

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.

Equations

• Condensed C = CategoryTheory.Sheaf (CategoryTheory.coherentTopology CompHaus) C

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

Equations

• instCategoryCondensed = let_fun this := inferInstance; this

@[inline, reducible]

abbrev CondensedSet : Type (u + 2)

Condensed sets (types) with the appropriate universe levels, i.e. Type (u+1)-valued sheaves on CompHaus.{u}.

Equations

• CondensedSet = Condensed (Type (u + 1))