Mathlib.Topology.Category.TopCat.ULift

TopCat.uliftFunctor definition

: TopCat.{u} ⥤ TopCat.{max u v}

Full source

/-- The functor which sends a topological space in `Type u` to a homeomorphic
space in `Type (max u v)`. -/
def uliftFunctor : TopCatTopCat.{u}TopCat.{u} ⥤ TopCat.{max u v} where
  obj X := TopCat.of (ULift.{v} X)
  map {X Y} f := ofHom ⟨ULift.map f, by continuity⟩

Lifting functor for topological spaces

Informal description

The functor that lifts a topological space $X$ of type `Type u` to a homeomorphic space of type `Type (max u v)`. Specifically, it maps $X$ to the topological space structure on `ULift.{v} X`, and for any continuous map $f : X \to Y$, it maps $f$ to the lifted continuous map `ULift.map f`.

TopCat.uliftFunctorObjHomeo definition

(X : TopCat.{u}) : X ≃ₜ uliftFunctor.{v}.obj X

Full source

/-- Given `X : TopCat.{u}`, this is the homeomorphism `X ≃ₜ uliftFunctor.{v}.obj X`. -/
def uliftFunctorObjHomeo (X : TopCatTopCat.{u}) : X ≃ₜ uliftFunctor.{v}.obj X :=
  Homeomorph.ulift.symm

Homeomorphism between a topological space and its lifted version

Informal description

For any topological space $ X $, this is the homeomorphism $ X \simeq \text{ULift}\, X $, where $\text{ULift}\, X$ is the lifted version of $ X $ to a higher universe.

TopCat.uliftFunctorObjHomeo_naturality_apply theorem

 {X Y : TopCat.{u}} (f : X ⟶ Y) (x : X) :
  uliftFunctor.{v}.map f (X.uliftFunctorObjHomeo x) = Y.uliftFunctorObjHomeo (f x)

Full source

@[simp]
lemma uliftFunctorObjHomeo_naturality_apply {X Y : TopCatTopCat.{u}} (f : X ⟶ Y) (x : X) :
    uliftFunctor.{v}.map f (X.uliftFunctorObjHomeo x) =
      Y.uliftFunctorObjHomeo (f x) := rfl

Naturality of Homeomorphism under Lifting Functor

Informal description

For any continuous map $f \colon X \to Y$ between topological spaces $X$ and $Y$, and for any point $x \in X$, the image of $x$ under the lifted map $\text{uliftFunctor}.map\, f$ composed with the homeomorphism $X \simeq \text{ULift}\, X$ equals the image of $f(x)$ under the homeomorphism $Y \simeq \text{ULift}\, Y$. In other words, the following diagram commutes: \[ \text{uliftFunctor}.map\, f \circ \text{uliftFunctorObjHomeo}_X(x) = \text{uliftFunctorObjHomeo}_Y(f(x)). \]

TopCat.uliftFunctorObjHomeo_symm_naturality_apply theorem

 {X Y : TopCat.{u}} (f : X ⟶ Y) (x : uliftFunctor.{v}.obj X) :
  Y.uliftFunctorObjHomeo.symm (uliftFunctor.{v}.map f x) = f (X.uliftFunctorObjHomeo.symm x)

Full source

@[simp]
lemma uliftFunctorObjHomeo_symm_naturality_apply {X Y : TopCatTopCat.{u}} (f : X ⟶ Y)
    (x : uliftFunctor.{v}.obj X) :
    Y.uliftFunctorObjHomeo.symm (uliftFunctor.{v}.map f x) =
      f (X.uliftFunctorObjHomeo.symm x) :=
  rfl

Naturality of Inverse Homeomorphism under Lifting Functor

Informal description

For any continuous map $f \colon X \to Y$ between topological spaces $X$ and $Y$, and for any point $x$ in the lifted space $\text{ULift}\, X$, the following equality holds: \[ \text{uliftFunctorObjHomeo}_Y^{-1} \big(\text{uliftFunctor.map}\, f (x)\big) = f \big(\text{uliftFunctorObjHomeo}_X^{-1}(x)\big). \] Here, $\text{uliftFunctorObjHomeo}_X^{-1}$ denotes the inverse of the homeomorphism between $X$ and its lifted version $\text{ULift}\, X$.

TopCat.uliftFunctorCompForgetIso definition

: uliftFunctor.{v, u} ⋙ forget TopCat.{max u v} ≅ forget TopCat.{u} ⋙ CategoryTheory.uliftFunctor.{v, u}

Full source

/-- The `ULift` functor on categories of topological spaces is compatible
with the one defined on categories of types. -/
@[simps!]
def uliftFunctorCompForgetIso : uliftFunctoruliftFunctor.{v, u}uliftFunctor.{v, u} ⋙ forget TopCat.{max u v}uliftFunctor.{v, u} ⋙ forget TopCat.{max u v} ≅
  forget TopCat.{u} ⋙ CategoryTheory.uliftFunctor.{v, u} := Iso.refl _

Isomorphism between lifting and forgetting functors for topological spaces

Informal description

The isomorphism between the composition of the lifting functor for topological spaces followed by the forgetful functor, and the composition of the forgetful functor followed by the type lifting functor. Specifically, it states that lifting a topological space and then forgetting its structure is isomorphic to forgetting the structure first and then lifting the underlying type.

TopCat.uliftFunctorFullyFaithful definition

: uliftFunctor.{v, u}.FullyFaithful

Full source

/-- The `ULift` functor on categories of topological spaces is fully faithful. -/
def uliftFunctorFullyFaithful : uliftFunctor.{v, u}.FullyFaithful where
  preimage f := ofHom ⟨ULift.down ∘ f ∘ ULift.up, by continuity⟩

Fully faithful lifting functor for topological spaces

Informal description

The functor `uliftFunctor` that lifts topological spaces to a higher universe is fully faithful, meaning it is both full (surjective on morphisms) and faithful (injective on morphisms).

TopCat.instFullUliftFunctor instance

: uliftFunctor.{v, u}.Full

Full source

instance : uliftFunctor.{v, u}.Full :=
  uliftFunctorFullyFaithful.full

The Lifting Functor for Topological Spaces is Full

Informal description

The lifting functor for topological spaces is full. That is, for any two topological spaces $X$ and $Y$ in `Type u`, every continuous map between their lifted versions in `Type (max u v)` is the image of a continuous map between $X$ and $Y$.

TopCat.instFaithfulUliftFunctor instance

: uliftFunctor.{v, u}.Faithful

Full source

instance : uliftFunctor.{v, u}.Faithful :=
  uliftFunctorFullyFaithful.faithful

Faithfulness of the Topological Space Lifting Functor

Informal description

The lifting functor for topological spaces is faithful. That is, for any two topological spaces $X$ and $Y$ in `Type u`, the map between the sets of continuous maps induced by the lifting functor is injective.