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
🔸 coverage
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).

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

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

    Instances For
      source
      📐 coverage
      @[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
      📐 coverage
      @[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
      🔸 coverage
      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.

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

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

        Instances For
          source
          📐 coverage
          instance TopCat.instFullUliftFunctor :
          uliftFunctor.Full
          source
          📐 coverage
          instance TopCat.instFaithfulUliftFunctor :
          uliftFunctor.Faithful
          source
          📐 coverage
          instance TopCat.instPreservesLimitsOfSizeUliftFunctor :
          CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} uliftFunctor
          source
          📐 coverage
          instance TopCat.instPreservesColimitsOfSizeUliftFunctor :
          CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} uliftFunctor