The functor from topological spaces to light condensed sets #
We define the functor topCatToLightCondSet : TopCat.{u} ⥤ LightCondSet.{u}
.
Projects #
- Prove that
topCatToLightCondSet
is faithful. - Define sequential topological spaces.
- Prove that
topCatToLightCondSet
restricted to sequential spaces is fully faithful. - Define the left adjoint of the restriction mentioned in the previous point.
Associate to a u
-small topological space the corresponding light condensed set, given by
yonedaPresheaf
.
Equations
- X.toLightCondSet = LightCondSet.ofSheafLightProfinite (ContinuousMap.yonedaPresheaf LightProfinite.toTopCat ↑X) ⋯
Instances For
TopCat.toLightCondSet
yields a functor from TopCat.{u}
to LightCondSet.{u}
.
Equations
- One or more equations did not get rendered due to their size.