Functors from categories of topological spaces to condensed sets

This file defines the embedding of the test objects (compact Hausdorff spaces) into condensed sets.

Main definitions

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

TODO (Dagur):

• 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}

instance instFullCondensedTypeCondensedSetUlift : Condensed.ulift.Full

Equations

• instFullCondensedTypeCondensedSetUlift = ⋯

instance instFaithfulCondensedTypeCondensedSetUlift : Condensed.ulift.Faithful

Equations

• instFaithfulCondensedTypeCondensedSetUlift = ⋯

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

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

Equations

• compHausToCondensed' = compHausToCondensed'.proof_1.yoneda

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

instance instFullCompHausCondensedTypeCompHausToCondensed' : compHausToCondensed'.Full

Equations

• instFullCompHausCondensedTypeCompHausToCondensed' = ⋯

instance instFaithfulCompHausCondensedTypeCompHausToCondensed' : compHausToCondensed'.Faithful

Equations

• instFaithfulCompHausCondensedTypeCompHausToCondensed' = ⋯

instance instFullCompHausCondensedSetCompHausToCondensed : compHausToCondensed.Full

Equations

• instFullCompHausCondensedSetCompHausToCondensed = ⋯

instance instFaithfulCompHausCondensedSetCompHausToCondensed : compHausToCondensed.Faithful

Equations

• instFaithfulCompHausCondensedSetCompHausToCondensed = ⋯