Functors from categories of topological spaces to condensed sets #
This file defines the embedding of the test objects (compact Hausdorff spaces) into condensed sets.
Main definitions #
compHausToCondensed : CompHaus.{u} тед CondensedSet.{u}
is essentially the yoneda presheaf functor. We also defineprofiniteToCondensed
andstoneanToCondensed
.
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
Instances For
The yoneda presheaf as an actual condensed set.
Equations
Instances For
@[reducible, inline]
Dot notation for the value of compHausToCondensed
.
Equations
- S.toCondensed = compHausToCondensed.obj S
Instances For
The yoneda presheaf as a condensed set, restricted to profinite spaces.
Equations
Instances For
@[reducible, inline]
Dot notation for the value of profiniteToCondensed
.
Equations
- S.toCondensed = profiniteToCondensed.obj S
Instances For
The yoneda presheaf as a condensed set, restricted to Stonean spaces.
Equations
Instances For
@[reducible, inline]
Dot notation for the value of stoneanToCondensed
.
Equations
- S.toCondensed = stoneanToCondensed.obj S