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.

Equations

• X.underlyingTopologicalSpace = TopologicalSpace.coinduced (LightCondSet.coinducingCoprod✝ X) inferInstance

def LightCondSet.toTopCat (X : LightCondSet) : TopCat

The object part of the functor LightCondSet ⥤ TopCat

Equations

• X.toTopCat = TopCat.of (X.val.obj (Opposite.op (LightProfinite.of PUnit.{?u.11 + 1})))

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

Equations

• LightCondSet.toTopCatMap f = { toFun := f.val.app (Opposite.op (LightProfinite.of PUnit.{?u.31 + 1})), continuous_toFun := ⋯ }

@[simp]

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

def lightCondSetToTopCat : CategoryTheory.Functor LightCondSet TopCat

The functor LightCondSet ⥤ TopCat

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem lightCondSetToTopCat_obj (X : LightCondSet) : lightCondSetToTopCat.obj X = X.toTopCat

@[simp]

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

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

The counit of the adjunction lightCondSetToTopCat ⊣ topCatToLightCondSet

Equations

• LightCondSet.topCatAdjunctionCounit X = { toFun := fun (x : ↑X.toLightCondSet.toTopCat) => x.toFun PUnit.unit, continuous_toFun := ⋯ }

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).

Equations

• One or more equations did not get rendered due to their size.

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

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

The unit of the adjunction lightCondSetToTopCat ⊣ topCatToLightCondSet

Equations

• One or more equations did not get rendered due to their size.

@[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 := ⋯ }

@[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

noncomputable def LightCondSet.topCatAdjunction : lightCondSetToTopCat ⊣ topCatToLightCondSet

The adjunction lightCondSetToTopCat ⊣ topCatToLightCondSet

Equations

• One or more equations did not get rendered due to their size.

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

instance LightCondSet.instFaithfulTopCatTopCatToLightCondSet : topCatToLightCondSet.Faithful

instance LightCondSet.instSequentialSpaceαTopologicalSpaceToTopCat (X : LightCondSet) : SequentialSpace ↑X.toTopCat

instance LightCondSet.instSequentialSpaceαTopologicalSpaceObjTopCatLightCondSetToTopCat (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.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LightCondSet.sequentialToLightCondSet : CategoryTheory.Functor Sequential LightCondSet

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

Equations

• LightCondSet.sequentialToLightCondSet = Sequential.sequentialToTop.comp topCatToLightCondSet

noncomputable def LightCondSet.sequentialAdjunction : LightCondSet.lightCondSetToSequential ⊣ LightCondSet.sequentialToLightCondSet

The adjunction lightCondSetToTopCat ⊣ topCatToLightCondSet restricted to sequential spaces.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• LightCondSet.sequentialAdjunctionHomeo X = { toEquiv := LightCondSet.topCatAdjunctionCounitEquiv X, continuous_toFun := ⋯, continuous_invFun := ⋯ }

noncomputable def LightCondSet.sequentialAdjunctionCounitIso (X : Sequential) : LightCondSet.lightCondSetToSequential.obj (LightCondSet.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}.

Equations

• LightCondSet.sequentialAdjunctionCounitIso X = Sequential.isoOfHomeo (LightCondSet.sequentialAdjunctionHomeo X.toTop)

instance LightCondSet.instIsIsoFunctorSequentialCounitSequentialAdjunction : CategoryTheory.IsIso LightCondSet.sequentialAdjunction.counit

noncomputable def LightCondSet.fullyFaithfulSequentialToLightCondSet : LightCondSet.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}.

Equations

• LightCondSet.fullyFaithfulSequentialToLightCondSet = LightCondSet.sequentialAdjunction.fullyFaithfulROfIsIsoCounit