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_val_app_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✝) = a✝
          source
          @[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 = (TopCat.Hom.hom a✝) 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
          noncomputable instance instMonoidalLightProfiniteLightCondSetLightProfiniteToLightCondSet :
          lightProfiniteToLightCondSet.Monoidal

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

          Equations