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.

noncomputable def TopCat.toLightCondSet (X : TopCat) : LightCondSet

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) ⋯

noncomputable def topCatToLightCondSet : CategoryTheory.Functor TopCat LightCondSet

TopCat.toLightCondSet yields a functor from TopCat.{u} to LightCondSet.{u}.

Equations

• One or more equations did not get rendered due to their size.