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.

def instTopologicalSpaceObjOppositeCompHausValOpOfPUnit (X : CondensedSet) : TopologicalSpace (X.val.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.

Equations

• instTopologicalSpaceObjOppositeCompHausValOpOfPUnit X = TopologicalSpace.coinduced (CondensedSet.coinducingCoprod✝ X) inferInstance

def CondensedSet.toTopCat (X : CondensedSet) : TopCat

The object part of the functor CondensedSet ⥤ TopCat

Equations

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

theorem CondensedSet.continuous_coinducingCoprod (X : CondensedSet) {S : CompHaus} (x : X.val.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

Equations

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

@[simp]

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

def condensedSetToTopCat : CategoryTheory.Functor CondensedSet TopCat

The functor CondensedSet ⥤ TopCat

Equations

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

@[simp]

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

@[simp]

theorem condensedSetToTopCat_obj (X : CondensedSet) : condensedSetToTopCat.obj X = X.toTopCat

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

The counit of the adjunction condensedSetToTopCat ⊣ topCatToCondensedSet

Equations

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

@[simp]

theorem CondensedSet.topCatAdjunctionCounit_apply (X : TopCat) (x : ↑X.toCondensedSet.toTopCat) : (CondensedSet.topCatAdjunctionCounit X) x = x.toFun PUnit.unit

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

Equations

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

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

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

The unit of the adjunction condensedSetToTopCat ⊣ topCatToCondensedSet

Equations

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

@[simp]

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

@[simp]

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

noncomputable def CondensedSet.topCatAdjunction : condensedSetToTopCat ⊣ topCatToCondensedSet

The adjunction condensedSetToTopCat ⊣ topCatToCondensedSet

Equations

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

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

instance CondensedSet.instFaithfulTopCatTopCatToCondensedSet : topCatToCondensedSet.Faithful

instance CondensedSet.instUCompactlyGeneratedSpaceαTopologicalSpaceToTopCat (X : CondensedSet) : UCompactlyGeneratedSpace ↑X.toTopCat

instance CondensedSet.instUCompactlyGeneratedSpaceαTopologicalSpaceObjTopCatCondensedSetToTopCat (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.

Equations

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

noncomputable def CondensedSet.compactlyGeneratedToCondensedSet : CategoryTheory.Functor CompactlyGenerated CondensedSet

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

Equations

• CondensedSet.compactlyGeneratedToCondensedSet = CompactlyGenerated.compactlyGeneratedToTop.comp topCatToCondensedSet

noncomputable def CondensedSet.compactlyGeneratedAdjunction : CondensedSet.condensedSetToCompactlyGenerated ⊣ CondensedSet.compactlyGeneratedToCondensedSet

The adjunction condensedSetToTopCat ⊣ topCatToCondensedSet restricted to compactly generated spaces.

Equations

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

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

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

Equations

• CondensedSet.compactlyGeneratedAdjunctionCounitHomeo X = { toEquiv := CondensedSet.topCatAdjunctionCounitEquiv X, continuous_toFun := ⋯, continuous_invFun := ⋯ }

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

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

Equations

• CondensedSet.compactlyGeneratedAdjunctionCounitIso X = CompactlyGenerated.isoOfHomeo (CondensedSet.compactlyGeneratedAdjunctionCounitHomeo X.toTop)

instance CondensedSet.instIsIsoFunctorCompactlyGeneratedCounitCompactlyGeneratedAdjunction : CategoryTheory.IsIso CondensedSet.compactlyGeneratedAdjunction.counit

noncomputable def CondensedSet.fullyFaithfulCompactlyGeneratedToCondensedSet : CondensedSet.compactlyGeneratedToCondensedSet.FullyFaithful

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

Equations

• CondensedSet.fullyFaithfulCompactlyGeneratedToCondensedSet = CondensedSet.compactlyGeneratedAdjunction.fullyFaithfulROfIsIsoCounit