Documentation

Mathlib.Condensed.Light.Functors

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 #

source
def lightProfiniteToLightCondSet :
CategoryTheory.Functor LightProfinite LightCondSet

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

Equations
Instances For
    source
    @[reducible, inline]
    abbrev LightProfinite.toCondensed (S : LightProfinite) :
    LightCondSet

    Dot notation for the value of lightProfiniteToLightCondSet.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev lightProfiniteToLightCondSetFullyFaithful :
      lightProfiniteToLightCondSet.FullyFaithful

      lightProfiniteToLightCondSet is fully faithful.

      Equations
      Instances For
        source
        instance instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet :
        lightProfiniteToLightCondSet.Full
        source
        instance instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet :
        lightProfiniteToLightCondSet.Faithful
        source
        noncomputable def lightProfiniteToLightCondSetIsoTopCatToLightCondSet :
        lightProfiniteToLightCondSet ≅ LightProfinite.toTopCat.comp topCatToLightCondSet

        The functor from LightProfinite to LightCondSet factors through TopCat.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_hom_app_hom_apply_hom_hom (X : LightProfinite) (X✝ : LightProfiniteᵒᵖ) (f : C(↑((CompHausLike.compHausLikeToTop fun (X : TopCat) => TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X).obj (Opposite.unop X✝)), ↑(LightProfinite.toTopCat.obj X))) :
          TopCat.Hom.hom ((CategoryTheory.ConcreteCategory.hom ((lightProfiniteToLightCondSetIsoTopCatToLightCondSet.inv.app X).hom.app X✝)) f).hom = f
          source
          @[simp]
          theorem lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_hom_app_hom_apply_apply (X : LightProfinite) (X✝ : LightProfiniteᵒᵖ) (f : (lightProfiniteToLightCondSet.obj X).obj.obj X✝) (a : ↑(Opposite.unop X✝).toTop) :
          ((CategoryTheory.ConcreteCategory.hom ((lightProfiniteToLightCondSetIsoTopCatToLightCondSet.hom.app X).hom.app X✝)) f) a = (CategoryTheory.ConcreteCategory.hom f.hom) a
          source
          instance instPreservesLimitsOfShapeLightProfiniteLightCondSetLightProfiniteToLightCondSetOfCountableCategory {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.CountableCategory J] :
          CategoryTheory.Limits.PreservesLimitsOfShape J lightProfiniteToLightCondSet

          The functor from LightProfinite to LightCondSet preserves countable limits.

          source
          instance instPreservesFiniteLimitsLightProfiniteLightCondSetLightProfiniteToLightCondSet :
          CategoryTheory.Limits.PreservesFiniteLimits lightProfiniteToLightCondSet

          The functor from LightProfinite to LightCondSet preserves finite limits.

          source
          @[implicit_reducible]
          noncomputable instance instMonoidalLightProfiniteLightCondSetLightProfiniteToLightCondSet :
          lightProfiniteToLightCondSet.Monoidal

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

          Equations
          source
          instance instPreservesFiniteCoproductsLightProfiniteLightCondSetLightProfiniteToLightCondSet :
          CategoryTheory.Limits.PreservesFiniteCoproducts lightProfiniteToLightCondSet