Functors from categories of topological spaces to light condensed sets #
This file defines the embedding of the test objects (light profinite sets) into light condensed sets.
Main definitions #
lightProfiniteToLightCondSet : LightProfinite.{u} ⥤ LightCondSet.{u}
is the yoneda presheaf functor.
TODO (Dagur):
- Define the functor
Type u ⥤ LightCondSet.{u}
which takes a setX
to the presheaf given by mapping a light profinite spaceS
toLocallyConstant S X
, along with the isomorphism with the functor that goes throughTopCat.{u+1}
.
The functor from LightProfinite.{u}
to LightCondSet.{u}
given by the Yoneda sheaf.
Equations
Instances For
@[reducible, inline]
Dot notation for the value of lightProfiniteToLightCondSet
.
Equations
- S.toCondensed = lightProfiniteToLightCondSet.obj S
Instances For
@[reducible, inline]
lightProfiniteToLightCondSet
is fully faithful.
Equations
- lightProfiniteToLightCondSetFullyFaithful = lightProfiniteToLightCondSet.proof_2.yonedaFullyFaithful