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 #
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
Instances For
Equations
- instCategoryCondensed = inferInstance
@[reducible, inline]
Condensed sets (types) with the appropriate universe levels, i.e. Type (u+1)
-valued
sheaves on CompHaus.{u}
.
Equations
- CondensedSet = Condensed (Type (?u.3 + 1))
Instances For
@[simp]
@[simp]
theorem
Condensed.comp_val
{C : Type w}
[CategoryTheory.Category.{v, w} C]
{X : Condensed C}
{Y : Condensed C}
{Z : Condensed C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
(CategoryTheory.CategoryStruct.comp f g).val = CategoryTheory.CategoryStruct.comp f.val g.val
@[simp]
theorem
CondensedSet.hom_naturality_apply
{X : CondensedSet}
{Y : CondensedSet}
(f : X ⟶ Y)
{S : CompHausᵒᵖ}
{T : CompHausᵒᵖ}
(g : S ⟶ T)
(x : X.val.obj S)
:
f.val.app T (X.val.map g x) = Y.val.map g (f.val.app S x)