Documentation

Mathlib.Topology.Category.TopCat.ULift

Lifting topological spaces to a higher universe #

In this file, we construct the functor uliftFunctor.{v, u} : TopCat.{u} ⥤ TopCat.{max u v} which sends a topological space X : Type u to a homeomorphic space in Type (max u v).

source
def TopCat.uliftFunctor :
CategoryTheory.Functor TopCat TopCat

The functor which sends a topological space in Type u to a homeomorphic space in Type (max u v).

Equations
    Instances For
      source
      def TopCat.uliftFunctorObjHomeo (X : TopCat) :
      ↑X ≃ₜ ↑(uliftFunctor.obj X)

      Given X : TopCat.{u}, this is the homeomorphism X ≃ₜ uliftFunctor.{v}.obj X.

      Equations
        Instances For
          source
          @[simp]
          theorem TopCat.uliftFunctorObjHomeo_naturality_apply {X Y : TopCat} (f : X ⟶ Y) (x : ↑X) :
          (CategoryTheory.ConcreteCategory.hom (uliftFunctor.map f)) (X.uliftFunctorObjHomeo x) = Y.uliftFunctorObjHomeo ((CategoryTheory.ConcreteCategory.hom f) x)
          source
          @[simp]
          theorem TopCat.uliftFunctorObjHomeo_symm_naturality_apply {X Y : TopCat} (f : X ⟶ Y) (x : ↑(uliftFunctor.obj X)) :
          Y.uliftFunctorObjHomeo.symm ((CategoryTheory.ConcreteCategory.hom (uliftFunctor.map f)) x) = (CategoryTheory.ConcreteCategory.hom f) (X.uliftFunctorObjHomeo.symm x)
          source
          def TopCat.uliftFunctorCompForgetIso :
          uliftFunctor.comp (CategoryTheory.forget TopCat) ≅ (CategoryTheory.forget TopCat).comp CategoryTheory.uliftFunctor.{v, u}

          The ULift functor on categories of topological spaces is compatible with the one defined on categories of types.

          Equations
            Instances For
              source
              @[simp]
              theorem TopCat.uliftFunctorCompForgetIso_hom_app (X : TopCat) (a✝ : (uliftFunctor.comp (CategoryTheory.forget TopCat)).obj X) :
              uliftFunctorCompForgetIso.hom.app X a✝ = a✝
              source
              @[simp]
              theorem TopCat.uliftFunctorCompForgetIso_inv_app (X : TopCat) (a✝ : (uliftFunctor.comp (CategoryTheory.forget TopCat)).obj X) :
              uliftFunctorCompForgetIso.inv.app X a✝ = a✝
              source
              def TopCat.uliftFunctorFullyFaithful :
              uliftFunctor.FullyFaithful

              The ULift functor on categories of topological spaces is fully faithful.

              Equations
                Instances For
                  source
                  instance TopCat.instFullUliftFunctor :
                  uliftFunctor.Full
                  source
                  instance TopCat.instFaithfulUliftFunctor :
                  uliftFunctor.Faithful