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 topCatToCondensedSet : TopCat.{u + 1} ⥤ CondensedSet.{u}.

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

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

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) [CategoryTheory.EffectiveEpi π], CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan π π) G] (hq : ∀ (Z B : C) (π : Z ⟶ B) [CategoryTheory.EffectiveEpi π], Topology.IsQuotientMap ⇑(CategoryTheory.ConcreteCategory.hom (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.

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.

def TopCat.toSheafCompHausLike (P : TopCat → Prop) (X : TopCat) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) : have this := ⋯; CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w))

The sheaf on CompHausLike P of continuous maps to a topological space.

@[simp]

theorem TopCat.toSheafCompHausLike_obj_obj (P : TopCat → Prop) (X : TopCat) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) (X✝ : (CompHausLike P)ᵒᵖ) : (toSheafCompHausLike P X hs).obj.obj X✝ = C(↑((CompHausLike.compHausLikeToTop P).obj (Opposite.unop X✝)), ↑X)

@[simp]

theorem TopCat.toSheafCompHausLike_obj_map (P : TopCat → Prop) (X : TopCat) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) {X✝ Y✝ : (CompHausLike P)ᵒᵖ} (f : X✝ ⟶ Y✝) (g : C(↑((CompHausLike.compHausLikeToTop P).obj (Opposite.unop X✝)), ↑X)) : (toSheafCompHausLike P X hs).obj.map f g = g.comp (Hom.hom f.unop.hom)

noncomputable def topCatToSheafCompHausLike (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) : have this := ⋯; CategoryTheory.Functor TopCat (CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w)))

TopCat.toSheafCompHausLike yields a functor from TopCat.{max u w} to Sheaf (coherentTopology (CompHausLike.{u} P)) (Type (max u w)).

@[simp]

theorem topCatToSheafCompHausLike_obj (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) (X : TopCat) : (topCatToSheafCompHausLike P hs).obj X = TopCat.toSheafCompHausLike P X hs

@[simp]

theorem topCatToSheafCompHausLike_map_hom_app (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) {X✝ Y✝ : TopCat} (f : X✝ ⟶ Y✝) (x✝ : (CompHausLike P)ᵒᵖ) (g : (TopCat.toSheafCompHausLike P X✝ hs).obj.obj x✝) : ((topCatToSheafCompHausLike P hs).map f).hom.app x✝ g = (TopCat.Hom.hom f).comp g

@[reducible, inline]

noncomputable abbrev TopCat.toCondensedSet (X : TopCat) : CondensedSet

Associate to a (u + 1)-small topological space the corresponding condensed set, given by yonedaPresheaf.

@[reducible, inline]

noncomputable abbrev topCatToCondensedSet : CategoryTheory.Functor TopCat CondensedSet

TopCat.toCondensedSet yields a functor from TopCat.{u + 1} to CondensedSet.{u}.