Commit 2025-02-10 17:54 228f5b63

View on Github →

feat(Topology): the ULift functor (#20345) In this PR, we define the functor uliftFunctor.{v} : TopCat.{u} ⥤ TopCat.{max u v} which sends a topological space in Type u to a homeomorphic space in Type (max u v).

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean

Modified Mathlib/Topology/Algebra/Group/Basic.lean

Modified Mathlib/Topology/Algebra/Module/Equiv.lean

Modified Mathlib/Topology/Algebra/Monoid.lean

Modified Mathlib/Topology/Algebra/MulAction.lean

Modified Mathlib/Topology/Category/CompHaus/Basic.lean

Created Mathlib/Topology/Category/TopCat/ULift.lean

added def TopCat.uliftFunctor

added def TopCat.uliftFunctorCompForgetIso

added def TopCat.uliftFunctorFullyFaithful

added def TopCat.uliftFunctorObjHomeo

added theorem TopCat.uliftFunctorObjHomeo_naturality_apply

added theorem TopCat.uliftFunctorObjHomeo_symm_naturality_apply

Modified Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean

Modified Mathlib/Topology/Constructions.lean

deleted theorem continuous_uLift_down

deleted theorem continuous_uLift_up

added theorem continuous_uliftDown

added theorem continuous_uliftMap

added theorem continuous_uliftUp

Modified Mathlib/Topology/Homeomorph.lean