Functors from categories of topological spaces to condensed sets

This file defines the various functors from categories of topological spaces to condensed sets.

Main definitions

• compHausToCondensed : CompHaus.{u} ⥤ CondensedSet.{u} is essentially the yoneda presheaf functor. We also define profiniteToCondensed and stoneanToCondensed.

TODO (Dagur):

• Add the functor TopCat.{u+1} ⥤ CondensedSet.{u}. This is done in a draft PR which depends on the explicit sheaf condition for condensed sets.

• Define the analogues of compHausToCondensed for sheaves on Profinite and Stonean and provide the relevant isomorphisms with profiniteToCondensed and stoneanToCondensed.

• Define the functor Type (u+1) ⥤ CondensedSet.{u} which takes a set X to the presheaf given by mapping a compact Hausdorff space S to LocallyConstant S X, along with the isomorphism with the functor that goes through TopCat.{u+1}.

def Condensed.ulift : CategoryTheory.Functor (Condensed (Type u)) CondensedSet

Increase the size of the target category of condensed sets.

Equations

• Condensed.ulift = CategoryTheory.sheafCompose (CategoryTheory.coherentTopology CompHaus) CategoryTheory.uliftFunctor.{u + 1, u}

def compHausToCondensed' : CategoryTheory.Functor CompHaus (Condensed (Type u))

The functor from CompHaus to Condensed.{u} (Type u) given by the Yoneda sheaf.

Equations

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

def compHausToCondensed : CategoryTheory.Functor CompHaus CondensedSet

The yoneda presheaf as an actual condensed set.

Equations

• compHausToCondensed = compHausToCondensed'.comp Condensed.ulift

@[reducible, inline]

abbrev CompHaus.toCondensed (S : CompHaus) : CondensedSet

Dot notation for the value of compHausToCondensed.

Equations

• S.toCondensed = compHausToCondensed.obj S

def profiniteToCondensed : CategoryTheory.Functor Profinite CondensedSet

The yoneda presheaf as a condensed set, restricted to profinite spaces.

Equations

• profiniteToCondensed = profiniteToCompHaus.comp compHausToCondensed

@[reducible, inline]

abbrev Profinite.toCondensed (S : Profinite) : CondensedSet

Dot notation for the value of profiniteToCondensed.

Equations

• S.toCondensed = profiniteToCondensed.obj S

def stoneanToCondensed : CategoryTheory.Functor Stonean CondensedSet

The yoneda presheaf as a condensed set, restricted to Stonean spaces.

Equations

• stoneanToCondensed = Stonean.toCompHaus.comp compHausToCondensed

@[reducible, inline]

abbrev Stonean.toCondensed (S : Stonean) : CondensedSet

Dot notation for the value of stoneanToCondensed.

Equations

• S.toCondensed = stoneanToCondensed.obj S