Documentation

Mathlib.Condensed.Light.TopComparison

The functor from topological spaces to light condensed sets #

We define the functor topCatToLightCondSet : TopCat.{u} ⥤ LightCondSet.{u}.

source
@[simp]
theorem TopCat.toLightCondSet_val_map (X : TopCat) :
∀ {X_1 Y : LightProfiniteᵒᵖ} (f : X_1 ⟶ Y) (g : C(↑(LightProfinite.toTopCat.obj (Opposite.unop X_1)), ↑X)), X.toLightCondSet.val.map f g = g.comp f.unop
source
@[simp]
theorem TopCat.toLightCondSet_val_obj (X : TopCat) (X : LightProfiniteᵒᵖ) :
X✝.toLightCondSet.val.obj X = C(↑(Opposite.unop X).toCompHaus.toTop, ↑X✝)
source
noncomputable def TopCat.toLightCondSet (X : TopCat) :
LightCondSet

Associate to a u-small topological space the corresponding light condensed set, given by yonedaPresheaf.

Equations
Instances For
    source
    @[simp]
    theorem topCatToLightCondSet_map_val_app :
    ∀ {X Y : TopCat} (f : X ⟶ Y) (x : LightProfiniteᵒᵖ) (g : ((fun (X : TopCat) => X.toLightCondSet) X).val.obj x), (topCatToLightCondSet.map f).val.app x g = ContinuousMap.comp f g
    source
    @[simp]
    theorem topCatToLightCondSet_obj (X : TopCat) :
    topCatToLightCondSet.obj X = X.toLightCondSet
    source
    noncomputable def topCatToLightCondSet :
    CategoryTheory.Functor TopCat LightCondSet

    TopCat.toLightCondSet yields a functor from TopCat.{u} to LightCondSet.{u}.

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