The adjunction between light condensed sets and topological spaces

This file defines the functor lightCondSetToTopCat : LightCondSet.{u} ⥤ TopCat.{u} which is left adjoint to topCatToLightCondSet : TopCat.{u} ⥤ LightCondSet.{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 sequential spaces, and we conclude that the functor topCatToLightCondSet is fully faithful when restricted to sequential spaces.

def LightCondSet.underlyingTopologicalSpace (X : LightCondSet) : TopologicalSpace (X.val.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))

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

@[reducible, inline]

abbrev LightCondSet.toTopCat (X : LightCondSet) : TopCat

The object part of the functor LightCondSet ⥤ TopCat

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

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

The map part of the functor LightCondSet ⥤ TopCat

@[simp]

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

def lightCondSetToTopCat : CategoryTheory.Functor LightCondSet TopCat

The functor LightCondSet ⥤ TopCat

@[simp]

theorem lightCondSetToTopCat_map {X✝ Y✝ : LightCondSet} (f : X✝ ⟶ Y✝) : lightCondSetToTopCat.map f = LightCondSet.toTopCatMap f

@[simp]

theorem lightCondSetToTopCat_obj_carrier (X : LightCondSet) : ↑(lightCondSetToTopCat.obj X) = X.val.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))

noncomputable def LightCondSet.topCatAdjunctionCounit (X : TopCat) : X.toLightCondSet.toTopCat ⟶ X

The counit of the adjunction lightCondSetToTopCat ⊣ topCatToLightCondSet

noncomputable def LightCondSet.topCatAdjunctionCounitEquiv (X : TopCat) : ↑X.toLightCondSet.toTopCat ≃ ↑X

The counit of the adjunction lightCondSetToTopCat ⊣ topCatToLightCondSet is always bijective, but not an isomorphism in general (the inverse isn't continuous unless X is sequential).

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

noncomputable def LightCondSet.topCatAdjunctionUnit (X : LightCondSet) : X ⟶ X.toTopCat.toLightCondSet

The unit of the adjunction lightCondSetToTopCat ⊣ topCatToLightCondSet

@[simp]

theorem LightCondSet.topCatAdjunctionUnit_val_app_apply (X : LightCondSet) (S : LightProfiniteᵒᵖ) (x : X.val.obj S) (s : ↑((CompHausLike.compHausLikeToTop fun (X : TopCat) => TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X).obj (Opposite.unop S))) : (X.topCatAdjunctionUnit.val.app S x) s = X.val.map (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) s).op x

@[simp]

theorem LightCondSet.topCatAdjunctionUnit_val_app (X : LightCondSet) (S : LightProfiniteᵒᵖ) (x : X.val.obj S) : X.topCatAdjunctionUnit.val.app S x = { toFun := fun (s : ↑((CompHausLike.compHausLikeToTop fun (X : TopCat) => TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X).obj (Opposite.unop S))) => X.val.map (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) s).op x, continuous_toFun := ⋯ }

noncomputable def LightCondSet.topCatAdjunction : lightCondSetToTopCat ⊣ topCatToLightCondSet

The adjunction lightCondSetToTopCat ⊣ topCatToLightCondSet

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

instance LightCondSet.instFaithfulTopCatTopCatToLightCondSet : topCatToLightCondSet.Faithful

instance LightCondSet.instSequentialSpaceCarrierToTopCat (X : LightCondSet) : SequentialSpace ↑X.toTopCat

instance LightCondSet.instSequentialSpaceCarrierObjTopCatLightCondSetToTopCat (X : LightCondSet) : SequentialSpace ↑(lightCondSetToTopCat.obj X)

def LightCondSet.lightCondSetToSequential : CategoryTheory.Functor LightCondSet Sequential

The functor from light condensed sets to topological spaces lands in sequential spaces.

noncomputable def LightCondSet.sequentialToLightCondSet : CategoryTheory.Functor Sequential LightCondSet

The functor from topological spaces to light condensed sets restricted to sequential spaces.

noncomputable def LightCondSet.sequentialAdjunction : lightCondSetToSequential ⊣ sequentialToLightCondSet

The adjunction lightCondSetToTopCat ⊣ topCatToLightCondSet restricted to sequential spaces.

noncomputable def LightCondSet.sequentialAdjunctionHomeo (X : TopCat) [SequentialSpace ↑X] : ↑X.toLightCondSet.toTopCat ≃ₜ ↑X

The counit of the adjunction lightCondSetToSequential ⊣ sequentialToLightCondSet is a homeomorphism.

Note: for now, we only have ℕ∪{∞} as a light profinite set at universe level 0, which is why we can only prove this for X : TopCat.{0}.

noncomputable def LightCondSet.sequentialAdjunctionCounitIso (X : Sequential) : lightCondSetToSequential.obj (sequentialToLightCondSet.obj X) ≅ X

The counit of the adjunction lightCondSetToSequential ⊣ sequentialToLightCondSet is an isomorphism.

Note: for now, we only have ℕ∪{∞} as a light profinite set at universe level 0, which is why we can only prove this for X : Sequential.{0}.

instance LightCondSet.instIsIsoFunctorSequentialCounitSequentialAdjunction : CategoryTheory.IsIso sequentialAdjunction.counit

noncomputable def LightCondSet.fullyFaithfulSequentialToLightCondSet : sequentialToLightCondSet.FullyFaithful

The functor from topological spaces to light condensed sets restricted to sequential spaces is fully faithful.

Note: for now, we only have ℕ∪{∞} as a light profinite set at universe level 0, which is why we can only prove this for the functor Sequential.{0} ⥤ LightCondSet.{0}.