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.
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 = (CategoryTheory.coherentTopology LightProfinite).yonedaFullyFaithful