The functor from topological spaces to light condensed sets

We define the functor topCatToLightCondSet : TopCat.{u} ⥤ LightCondSet.{u}.

@[reducible, inline]

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

Associate to a u-small topological space the corresponding light condensed set, given by yonedaPresheaf.

Equations

• X.toLightCondSet = TopCat.toSheafCompHausLike (fun (X : TopCat) => TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X) X TopCat.toLightCondSet.proof_1

@[reducible, inline]

noncomputable abbrev topCatToLightCondSet : CategoryTheory.Functor TopCat LightCondSet

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

Equations

• topCatToLightCondSet = topCatToSheafCompHausLike (fun (X : TopCat) => TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X) topCatToLightCondSet.proof_1