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
  • One or more equations did not get rendered due to their size.
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
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          instance TopCat.instFullUliftFunctor :
          uliftFunctor.Full
          source
          instance TopCat.instFaithfulUliftFunctor :
          uliftFunctor.Faithful