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 #

source
🔸 coverage
def Condensed.ulift :
CategoryTheory.Functor (Condensed (Type u)) CondensedSet

Increase the size of the target category of condensed sets.

Instances For
    source
    📐 coverage
    instance instFullCondensedTypeCondensedSetUlift :
    Condensed.ulift.Full
    source
    📐 coverage
    instance instFaithfulCondensedTypeCondensedSetUlift :
    Condensed.ulift.Faithful
    source
    🔸 coverage
    def compHausToCondensed' :
    CategoryTheory.Functor CompHaus (Condensed (Type u))

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

    Instances For
      source
      🔸 coverage
      def compHausToCondensed :
      CategoryTheory.Functor CompHaus CondensedSet

      The yoneda presheaf as an actual condensed set.

      Instances For
        source
        🔸 coverage
        @[reducible, inline]
        abbrev CompHaus.toCondensed (S : CompHaus) :
        CondensedSet

        Dot notation for the value of compHausToCondensed.

        Instances For
          source
          🔸 coverage
          def profiniteToCondensed :
          CategoryTheory.Functor Profinite CondensedSet

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

          Instances For
            source
            🔸 coverage
            @[reducible, inline]
            abbrev Profinite.toCondensed (S : Profinite) :
            CondensedSet

            Dot notation for the value of profiniteToCondensed.

            Instances For
              source
              🔸 coverage
              def stoneanToCondensed :
              CategoryTheory.Functor Stonean CondensedSet

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

              Instances For
                source
                🔸 coverage
                @[reducible, inline]
                abbrev Stonean.toCondensed (S : Stonean) :
                CondensedSet

                Dot notation for the value of stoneanToCondensed.

                Instances For
                  source
                  📐 coverage
                  instance instFullCompHausCondensedTypeCompHausToCondensed' :
                  compHausToCondensed'.Full
                  source
                  📐 coverage
                  instance instFaithfulCompHausCondensedTypeCompHausToCondensed' :
                  compHausToCondensed'.Faithful
                  source
                  📐 coverage
                  instance instFullCompHausCondensedSetCompHausToCondensed :
                  compHausToCondensed.Full
                  source
                  📐 coverage
                  instance instFaithfulCompHausCondensedSetCompHausToCondensed :
                  compHausToCondensed.Faithful
                  source
                  📐 coverage
                  instance instPreservesFiniteCoproductsCompHausCondensedSetCompHausToCondensed :
                  CategoryTheory.Limits.PreservesFiniteCoproducts compHausToCondensed