Functors from categories of topological spaces to light condensed sets

This file defines the embedding of the test objects (light profinite sets) into light condensed sets.

Main definitions

• lightProfiniteToLightCondSet : LightProfinite.{u} ⥤ LightCondSet.{u} is the yoneda sheaf functor.

def lightProfiniteToLightCondSet : CategoryTheory.Functor LightProfinite LightCondSet

The functor from LightProfinite.{u} to LightCondSet.{u} given by the Yoneda sheaf.

@[reducible, inline]

abbrev LightProfinite.toCondensed (S : LightProfinite) : LightCondSet

Dot notation for the value of lightProfiniteToLightCondSet.

@[reducible, inline]

abbrev lightProfiniteToLightCondSetFullyFaithful : lightProfiniteToLightCondSet.FullyFaithful

lightProfiniteToLightCondSet is fully faithful.

instance instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet : lightProfiniteToLightCondSet.Full

instance instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet : lightProfiniteToLightCondSet.Faithful

noncomputable def lightProfiniteToLightCondSetIsoTopCatToLightCondSet : lightProfiniteToLightCondSet ≅ LightProfinite.toTopCat.comp topCatToLightCondSet

The functor from LightProfinite to LightCondSet factors through TopCat.

@[simp]

theorem lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_val_app_hom_hom (X : LightProfinite) (X✝ : LightProfiniteᵒᵖ) (a✝ : ((CategoryTheory.sheafToPresheaf (CategoryTheory.coherentTopology LightProfinite) (Type u)).obj ((LightProfinite.toTopCat.comp topCatToLightCondSet).obj X)).obj X✝) : TopCat.Hom.hom ((lightProfiniteToLightCondSetIsoTopCatToLightCondSet.inv.app X).val.app X✝ a✝).hom = a✝

@[simp]

theorem lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_val_app_apply (X : LightProfinite) (X✝ : LightProfiniteᵒᵖ) (a✝ : ((CategoryTheory.sheafToPresheaf (CategoryTheory.coherentTopology LightProfinite) (Type u)).obj (lightProfiniteToLightCondSet.obj X)).obj X✝) (a : ↑(Opposite.unop X✝).toTop) : ((lightProfiniteToLightCondSetIsoTopCatToLightCondSet.hom.app X).val.app X✝ a✝) a = (CategoryTheory.ConcreteCategory.hom a✝.hom) a

instance instPreservesLimitsOfShapeLightProfiniteLightCondSetLightProfiniteToLightCondSetOfCountableCategory {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.CountableCategory J] : CategoryTheory.Limits.PreservesLimitsOfShape J lightProfiniteToLightCondSet

The functor from LightProfinite to LightCondSet preserves countable limits.

instance instPreservesFiniteLimitsLightProfiniteLightCondSetLightProfiniteToLightCondSet : CategoryTheory.Limits.PreservesFiniteLimits lightProfiniteToLightCondSet

The functor from LightProfinite to LightCondSet preserves finite limits.

noncomputable instance instMonoidalLightProfiniteLightCondSetLightProfiniteToLightCondSet : lightProfiniteToLightCondSet.Monoidal

The functor from LightProfinite to LightCondSet is monoidal with respect to the cartesian monoidal structure.