The adjunction between condensed sets and topological spaces

This file defines the functor condensedSetToTopCat : CondensedSet.{u} ⥤ TopCat.{u + 1} which is left adjoint to topCatToCondensedSet : TopCat.{u + 1} ⥤ CondensedSet.{u}. We prove that the counit is bijective (but not in general an isomorphism) and conclude that the right adjoint is faithful.

The counit is an isomorphism for compactly generated spaces, and we conclude that the functor topCatToCondensedSet is fully faithful when restricted to compactly generated spaces.

@[implicit_reducible]

def instTopologicalSpaceObjOppositeCompHausObjFunctorTypeIsSheafCoherentTopologyOpOfPUnit (X : CondensedSet) : TopologicalSpace (X.obj.obj (Opposite.op (CompHaus.of PUnit.{u + 1})))

Let X be a condensed set. We define a topology on X(*) as the quotient topology of all the maps from compact Hausdorff S spaces to X(*), corresponding to elements of X(S). In other words, the topology coinduced by the map CondensedSet.coinducingCoprod above.

@[reducible, inline]

abbrev CondensedSet.toTopCat (X : CondensedSet) : TopCat

The object part of the functor CondensedSet ⥤ TopCat

theorem CondensedSet.continuous_coinducingCoprod (X : CondensedSet) {S : CompHaus} (x : X.obj.obj (Opposite.op S)) : Continuous fun (a : ↑⟨S, x⟩.fst.toTop) => CondensedSet.coinducingCoprod✝ X ⟨⟨S, x⟩, a⟩

def CondensedSet.toTopCatMap {X Y : CondensedSet} (f : X ⟶ Y) : X.toTopCat ⟶ Y.toTopCat

The map part of the functor CondensedSet ⥤ TopCat

@[simp]

theorem CondensedSet.toTopCatMap_hom_apply {X Y : CondensedSet} (f : X ⟶ Y) (a✝ : X.obj.obj (Opposite.op (CompHaus.of PUnit.{u + 1}))) : (TopCat.Hom.hom (toTopCatMap f)) a✝ = f.hom.app (Opposite.op (CompHaus.of PUnit.{u + 1})) a✝

def condensedSetToTopCat : CategoryTheory.Functor CondensedSet TopCat

The functor CondensedSet ⥤ TopCat

@[simp]

theorem condensedSetToTopCat_map {X✝ Y✝ : CondensedSet} (f : X✝ ⟶ Y✝) : condensedSetToTopCat.map f = CondensedSet.toTopCatMap f

@[simp]

theorem condensedSetToTopCat_obj_carrier (X : CondensedSet) : ↑(condensedSetToTopCat.obj X) = X.obj.obj (Opposite.op (CompHaus.of PUnit.{u + 1}))

noncomputable def CondensedSet.topCatAdjunctionCounit (X : TopCat) : X.toCondensedSet.toTopCat ⟶ X

The counit of the adjunction condensedSetToTopCat ⊣ topCatToCondensedSet

@[simp]

theorem CondensedSet.topCatAdjunctionCounit_hom_apply (X : TopCat) (x : C(PUnit.{u_1 + 1}, ↑X)) : (TopCat.Hom.hom (topCatAdjunctionCounit X)) x = x PUnit.unit

simp-normal form of the lemma that @[simps] would generate.

noncomputable def CondensedSet.topCatAdjunctionCounitEquiv (X : TopCat) : ↑X.toCondensedSet.toTopCat ≃ ↑X

The counit of the adjunction condensedSetToTopCat ⊣ topCatToCondensedSet is always bijective, but not an isomorphism in general (the inverse isn't continuous unless X is compactly generated).

theorem CondensedSet.topCatAdjunctionCounit_bijective (X : TopCat) : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (topCatAdjunctionCounit X))

noncomputable def CondensedSet.topCatAdjunctionUnit (X : CondensedSet) : X ⟶ X.toTopCat.toCondensedSet

The unit of the adjunction condensedSetToTopCat ⊣ topCatToCondensedSet

@[simp]

theorem CondensedSet.topCatAdjunctionUnit_hom_app_apply (X : CondensedSet) (S : CompHausᵒᵖ) (x : X.obj.obj S) (s : ↑((CompHausLike.compHausLikeToTop fun (x : TopCat) => True).obj (Opposite.unop S))) : (X.topCatAdjunctionUnit.hom.app S x) s = X.obj.map (CompHausLike.const (CompHaus.of PUnit.{u + 1}) s).op x

@[simp]

theorem CondensedSet.topCatAdjunctionUnit_hom_app (X : CondensedSet) (S : CompHausᵒᵖ) (x : X.obj.obj S) : X.topCatAdjunctionUnit.hom.app S x = { toFun := fun (s : ↑((CompHausLike.compHausLikeToTop fun (x : TopCat) => True).obj (Opposite.unop S))) => X.obj.map (CompHausLike.const (CompHaus.of PUnit.{u + 1}) s).op x, continuous_toFun := ⋯ }

noncomputable def CondensedSet.topCatAdjunction : condensedSetToTopCat ⊣ topCatToCondensedSet

The adjunction condensedSetToTopCat ⊣ topCatToCondensedSet

instance CondensedSet.instEpiTopCatAppCounitTopCatAdjunction (X : TopCat) : CategoryTheory.Epi (topCatAdjunction.counit.app X)

instance CondensedSet.instFaithfulTopCatTopCatToCondensedSet : topCatToCondensedSet.Faithful

instance CondensedSet.instUCompactlyGeneratedSpaceCarrierToTopCat (X : CondensedSet) : UCompactlyGeneratedSpace ↑X.toTopCat

instance CondensedSet.instUCompactlyGeneratedSpaceCarrierObjTopCatCondensedSetToTopCat (X : CondensedSet) : UCompactlyGeneratedSpace ↑(condensedSetToTopCat.obj X)

def CondensedSet.condensedSetToCompactlyGenerated : CategoryTheory.Functor CondensedSet CompactlyGenerated

The functor from condensed sets to topological spaces lands in compactly generated spaces.

noncomputable def CondensedSet.compactlyGeneratedToCondensedSet : CategoryTheory.Functor CompactlyGenerated CondensedSet

The functor from topological spaces to condensed sets restricted to compactly generated spaces.

noncomputable def CondensedSet.compactlyGeneratedAdjunction : condensedSetToCompactlyGenerated ⊣ compactlyGeneratedToCondensedSet

The adjunction condensedSetToTopCat ⊣ topCatToCondensedSet restricted to compactly generated spaces.

noncomputable def CondensedSet.compactlyGeneratedAdjunctionCounitHomeo (X : TopCat) [UCompactlyGeneratedSpace ↑X] : ↑X.toCondensedSet.toTopCat ≃ₜ ↑X

The counit of the adjunction condensedSetToCompactlyGenerated ⊣ compactlyGeneratedToCondensedSet is a homeomorphism.

noncomputable def CondensedSet.compactlyGeneratedAdjunctionCounitIso (X : CompactlyGenerated) : condensedSetToCompactlyGenerated.obj (compactlyGeneratedToCondensedSet.obj X) ≅ X

The counit of the adjunction condensedSetToCompactlyGenerated ⊣ compactlyGeneratedToCondensedSet is an isomorphism.

instance CondensedSet.instIsIsoFunctorCompactlyGeneratedCounitCompactlyGeneratedAdjunction : CategoryTheory.IsIso compactlyGeneratedAdjunction.counit

noncomputable def CondensedSet.fullyFaithfulCompactlyGeneratedToCondensedSet : compactlyGeneratedToCondensedSet.FullyFaithful

The functor from topological spaces to condensed sets restricted to compactly generated spaces is fully faithful.