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 #

TODO (Dagur):

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

Equations
Instances For
    @[reducible, inline]

    Dot notation for the value of lightProfiniteToLightCondSet.

    Equations
    Instances For