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 set X to the presheaf given by mapping a light profinite space S to LocallyConstant S X, along with the isomorphism with the functor that goes through TopCat.{u+1}.

def lightProfiniteToLightCondSet : CategoryTheory.Functor LightProfinite LightCondSet

The functor from LightProfinite.{u} to LightCondSet.{u} given by the Yoneda sheaf.

Equations

• lightProfiniteToLightCondSet = ⋯.yoneda

@[reducible, inline]

abbrev LightProfinite.toCondensed (S : LightProfinite) : LightCondSet

Dot notation for the value of lightProfiniteToLightCondSet.

Equations

• S.toCondensed = lightProfiniteToLightCondSet.obj S

@[reducible, inline]

abbrev lightProfiniteToLightCondSetFullyFaithful : lightProfiniteToLightCondSet.FullyFaithful

lightProfiniteToLightCondSet is fully faithful.

Equations

• lightProfiniteToLightCondSetFullyFaithful = ⋯.yonedaFullyFaithful

instance instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet : lightProfiniteToLightCondSet.Full

Equations

• instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet = ⋯

instance instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet : lightProfiniteToLightCondSet.Faithful

Equations

• instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet = ⋯