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.

def lightProfiniteToLightCondSet : CategoryTheory.Functor LightProfinite LightCondSet

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

Equations

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

instance instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet : lightProfiniteToLightCondSet.Full

instance instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet : lightProfiniteToLightCondSet.Faithful