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
def Condensed.ulift :
CategoryTheory.Functor (Condensed (Type u)) CondensedSet

Increase the size of the target category of condensed sets.

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

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

      Equations
        Instances For
          source
          def compHausToCondensed :
          CategoryTheory.Functor CompHaus CondensedSet

          The yoneda presheaf as an actual condensed set.

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

              Dot notation for the value of compHausToCondensed.

              Equations
                Instances For
                  source
                  def profiniteToCondensed :
                  CategoryTheory.Functor Profinite CondensedSet

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

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

                      Dot notation for the value of profiniteToCondensed.

                      Equations
                        Instances For
                          source
                          def stoneanToCondensed :
                          CategoryTheory.Functor Stonean CondensedSet

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

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

                              Dot notation for the value of stoneanToCondensed.

                              Equations
                                Instances For
                                  source
                                  instance instFullCompHausCondensedTypeCompHausToCondensed' :
                                  compHausToCondensed'.Full
                                  source
                                  instance instFaithfulCompHausCondensedTypeCompHausToCondensed' :
                                  compHausToCondensed'.Faithful
                                  source
                                  instance instFullCompHausCondensedSetCompHausToCondensed :
                                  compHausToCondensed.Full
                                  source
                                  instance instFaithfulCompHausCondensedSetCompHausToCondensed :
                                  compHausToCondensed.Faithful