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.

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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 + 1))

theorem Condensed.hom_ext {C : Type w} [CategoryTheory.Category.{v, w} C] {X Y : Condensed C} (f g : X ⟶ Y) (h : ∀ (S : CompHausᵒᵖ), f.hom.app S = g.hom.app S) : f = g

theorem Condensed.hom_ext_iff {C : Type w} [CategoryTheory.Category.{v, w} C] {X Y : Condensed C} {f g : X ⟶ Y} : f = g ↔ ∀ (S : CompHausᵒᵖ), f.hom.app S = g.hom.app S