The functor from topological spaces to condensed sets #

This file builds on the API from the file TopCat.Yoneda. If the forgetful functor to TopCat has nice properties, like preserving pullbacks and finite coproducts, then this Yoneda presheaf satisfies the sheaf condition for the regular and extensive topologies respectively.

We apply this API to CompHaus and define the functor topCatToCondensed : TopCat.{u+1} ⥤ CondensedSet.{u}.

Projects #

Prove that topCatToCondensed is faithful.
Define compactly generated topological spaces.
Prove that topCatToCondensed restricted to compactly generated spaces is fully faithful.
Define the left adjoint of the restriction mentioned in the previous point.

source

theorem factorsThrough_of_pullbackCondition {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C TopCat) (X : Type w') [TopologicalSpace X] {Z : C} {B : C} {π : Z ⟶ B} [CategoryTheory.Limits.HasPullback π π] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan π π) G] {a : C(↑(G.obj Z), X)} (ha : ⇑a ∘ ⇑(G.map CategoryTheory.Limits.pullback.fst) = ⇑a ∘ ⇑(G.map CategoryTheory.Limits.pullback.snd)) :

Function.FactorsThrough ⇑a ⇑(G.map π)

An auxiliary lemma to that allows us to use QuotientMap.lift in the proof of equalizerCondition_yonedaPresheaf.

source

theorem equalizerCondition_yonedaPresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C TopCat) (X : Type w') [TopologicalSpace X] [(Z B : C) → (π : Z ⟶ B) → [inst : CategoryTheory.EffectiveEpi π] → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan π π) G] (hq : ∀ (Z B : C) (π : Z ⟶ B) [inst : CategoryTheory.EffectiveEpi π], QuotientMap ⇑(G.map π)) :

CategoryTheory.regularTopology.EqualizerCondition (ContinuousMap.yonedaPresheaf G X)

If G preserves the relevant pullbacks and every effective epi in C is a quotient map (which is the case when C is CompHaus or Profinite), then yonedaPresheaf satisfies the equalizer condition which is required to be a sheaf for the regular topology.

source

noncomputable instance instPreservesFiniteProductsOppositeYonedaPresheafOfPreservesFiniteCoproductsTopCat {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C TopCat) (X : Type w') [TopologicalSpace X] [CategoryTheory.Limits.PreservesFiniteCoproducts G] :

CategoryTheory.Limits.PreservesFiniteProducts (ContinuousMap.yonedaPresheaf G X)

If G preserves finite coproducts (which is the case when C is CompHaus, Profinite or Stonean), then yonedaPresheaf preserves finite products, which is required to be a sheaf for the extensive topology.

Equations