Functors from categories of topological spaces to condensed sets #
This file defines the various functors from catgegories of topological spaces to condensed sets.
Main definitions #
compHausToCondensed : CompHaus.{u} ⥤ CondensedSet.{u}
is essentially the yoneda presheaf functor. We also defineprofiniteToCondensed
andstoneanToCondensed
.
TODO (Dagur):

Add the functor
TopCat.{u+1} ⥤ CondensedSet.{u}
. This is done in a draft PR which depends on the explicit sheaf condition for condensed sets. 
Define the analogues of
compHausToCondensed
for sheaves onProfinite
andStonean
and provide the relevant isomorphisms withprofiniteToCondensed
andstoneanToCondensed
. 
Define the functor
Type (u+1) ⥤ CondensedSet.{u}
which takes a setX
to the presheaf given by mapping a compact Hausdorff spaceS
toLocallyConstant S X
, along with the isomorphism with the functor that goes throughTopCat.{u+1}
.
Increase the size of the target category of condensed sets.
Equations
Instances For
The functor from CompHaus
to Condensed.{u} (Type u)
given by the Yoneda sheaf.
Equations
 One or more equations did not get rendered due to their size.
Instances For
The yoneda presheaf as an actual condensed set.
Instances For
Dot notation for the value of compHausToCondensed
.
Equations
 CompHaus.toCondensed S = compHausToCondensed.obj S
Instances For
The yoneda presheaf as a condensed set, restricted to profinite spaces.
Instances For
The yoneda presheaf as a condensed set, restricted to Stonean spaces.
Instances For
Dot notation for the value of stoneanToCondensed
.
Equations
 Stonean.toCondensed S = stoneanToCondensed.obj S