Documentation

Mathlib.Condensed.Functors

Functors from categories of topological spaces to condensed sets #

This file defines the embedding of the test objects (compact Hausdorff spaces) into condensed sets.

Main definitions #

The functor from CompHaus to Condensed.{u} (Type u) given by the Yoneda sheaf.

Equations
Instances For

    The yoneda presheaf as an actual condensed set.

    Equations
    Instances For
      @[reducible, inline]

      Dot notation for the value of compHausToCondensed.

      Equations
      Instances For

        The yoneda presheaf as a condensed set, restricted to profinite spaces.

        Equations
        Instances For
          @[reducible, inline]

          Dot notation for the value of profiniteToCondensed.

          Equations
          Instances For

            The yoneda presheaf as a condensed set, restricted to Stonean spaces.

            Equations
            Instances For
              @[reducible, inline]

              Dot notation for the value of stoneanToCondensed.

              Equations
              Instances For