Documentation

Mathlib.Condensed.TopCatAdjunction

The adjunction between condensed sets and topological spaces #

This file defines the functor condensedSetToTopCat : CondensedSet.{u} ⥤ TopCat.{u+1} which is left adjoint to topCatToCondensedSet : TopCat.{u+1} ⥤ CondensedSet.{u}. We prove that the counit is bijective (but not in general an isomorphism) and conclude that the right adjoint is faithful.

The counit is an isomorphism for compactly generated spaces, and we conclude that the functor topCatToCondensedSet is fully faithful when restricted to compactly generated spaces.

Let X be a condensed set. We define a topology on X(*) as the quotient topology of all the maps from compact Hausdorff S spaces to X(*), corresponding to elements of X(S). In other words, the topology coinduced by the map CondensedSet.coinducingCoprod above.

Equations
Instances For

    The object part of the functor CondensedSetTopCat

    Equations
    Instances For
      theorem CondensedSet.continuous_coinducingCoprod (X : CondensedSet) {S : CompHaus} (x : X.val.obj (Opposite.op S)) :
      Continuous fun (a : S, x.fst.toTop) => CondensedSet.coinducingCoprod X S, x, a
      def CondensedSet.toTopCatMap {X : CondensedSet} {Y : CondensedSet} (f : X Y) :
      X.toTopCat Y.toTopCat

      The map part of the functor CondensedSetTopCat

      Equations
      Instances For
        @[simp]

        The functor CondensedSetTopCat

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem CondensedSet.topCatAdjunctionCounit_apply (X : TopCat) (x : X.toCondensedSet.toTopCat) :
          def CondensedSet.topCatAdjunctionCounit (X : TopCat) :
          X.toCondensedSet.toTopCat X

          The counit of the adjunction condensedSetToTopCattopCatToCondensedSet

          Equations
          Instances For
            def CondensedSet.topCatAdjunctionCounitEquiv (X : TopCat) :
            X.toCondensedSet.toTopCat X

            The counit of the adjunction condensedSetToTopCattopCatToCondensedSet is always bijective, but not an isomorphism in general (the inverse isn't continuous unless X is compactly generated).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem CondensedSet.topCatAdjunctionUnit_val_app (X : CondensedSet) (S : CompHausᵒᵖ) (x : X.val.obj S) :
              X.topCatAdjunctionUnit.val.app S x = { toFun := fun (s : ((CompHausLike.compHausLikeToTop fun (x : TopCat) => True).obj (Opposite.unop S))) => X.val.map (CompHaus.const (Opposite.unop S) s).op x, continuous_toFun := }
              @[simp]
              theorem CondensedSet.topCatAdjunctionUnit_val_app_apply (X : CondensedSet) (S : CompHausᵒᵖ) (x : X.val.obj S) (s : ((CompHausLike.compHausLikeToTop fun (x : TopCat) => True).obj (Opposite.unop S))) :
              (X.topCatAdjunctionUnit.val.app S x) s = X.val.map (CompHaus.const (Opposite.unop S) s).op x
              def CondensedSet.topCatAdjunctionUnit (X : CondensedSet) :
              X X.toTopCat.toCondensedSet

              The unit of the adjunction condensedSetToTopCattopCatToCondensedSet

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                The adjunction condensedSetToTopCattopCatToCondensedSet

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  The functor from condensed sets to topological spaces lands in compactly generated spaces.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    The functor from topological spaces to condensed sets restricted to compactly generated spaces.

                    Equations
                    Instances For

                      The adjunction condensedSetToTopCattopCatToCondensedSet restricted to compactly generated spaces.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        The counit of the adjunction condensedSetToCompactlyGeneratedcompactlyGeneratedToCondensedSet is a homeomorphism.

                        Equations
                        Instances For

                          The functor from topological spaces to condensed sets restricted to compactly generated spaces is fully faithful.

                          Equations
                          Instances For