feat(Topology/Category): TopCat.uliftFunctor preserves all limits and colimits

Mathlib/Topology/Category/TopCat/Limits/Basic.lean

@@ -136,6 +136,17 @@ theorem induced_of_isLimit :
 
 end IsLimit
 
+lemma nonempty_isLimit_iff_eq_induced {F : J ⥤ TopCat.{u}} (c : Cone F)
+    (hc : IsLimit ((forget).mapCone c)) :
+    Nonempty (IsLimit c) ↔ c.pt.str = ⨅ j, (F.obj j).str.induced (c.π.app j) := by
+  refine ⟨fun ⟨hc⟩ ↦ induced_of_isLimit _ hc, fun h ↦ ⟨?_⟩⟩
+  refine .ofIsoLimit (isLimitConeOfForget _ hc) (Cones.ext ?_ ?_)
+  · refine TopCat.isoOfHomeo
+      { toEquiv := .refl _,
+        continuous_toFun := h ▸ by fun_prop,
+        continuous_invFun := h ▸ by fun_prop }
+  · intro; rfl
+
 variable (F : J ⥤ TopCat.{u})
 
 theorem limit_topology [HasLimit F] :
@@ -253,6 +264,16 @@ lemma continuous_iff_of_isColimit {X : Type u'} [TopologicalSpace X] (f : c.pt 
 
 end IsColimit
 
+lemma nonempty_isColimit_iff_eq_coinduced (c : Cocone F) (hc : IsColimit ((forget).mapCocone c)) :
+    Nonempty (IsColimit c) ↔ c.pt.str = ⨆ j, (F.obj j).str.coinduced (c.ι.app j) := by
+  refine ⟨fun ⟨hc⟩ ↦ coinduced_of_isColimit _ hc, fun h ↦ ⟨?_⟩⟩
+  refine .ofIsoColimit (isColimitCoconeOfForget _ hc) (Cocones.ext ?_ ?_)
+  · refine TopCat.isoOfHomeo
+      { toEquiv := .refl _,
+        continuous_toFun := h ▸ by fun_prop,
+        continuous_invFun := h ▸ by fun_prop }
+  · intro; rfl
+
 variable (F)
 
 theorem colimit_topology (F : J ⥤ TopCat.{u}) [HasColimit F] :

Mathlib/Topology/Category/TopCat/ULift.lean

@@ -5,8 +5,9 @@ Authors: Joël Riou
 -/
 module
 
-public import Mathlib.Topology.Category.TopCat.Basic
+public import Mathlib.Topology.Category.TopCat.Limits.Basic
 public import Mathlib.Topology.Homeomorph.Lemmas
+public import Mathlib.CategoryTheory.Limits.Preserves.Ulift
 
 /-!
 # Lifting topological spaces to a higher universe
@@ -18,7 +19,7 @@ which sends a topological space `X : Type u` to a homeomorphic space in `Type (m
 
 @[expose] public section
 
-universe v u
+universe w w' v u
 
 open CategoryTheory
 
@@ -65,4 +66,34 @@ instance : uliftFunctor.{v, u}.Full :=
 instance : uliftFunctor.{v, u}.Faithful :=
   uliftFunctorFullyFaithful.faithful
 
+open Limits
+
+instance : PreservesLimitsOfSize.{w', w} uliftFunctor.{v, u} := by
+  refine ⟨⟨fun {K} ↦ ⟨fun {c} hc ↦ ?_⟩⟩⟩
+  rw [nonempty_isLimit_iff_eq_induced]
+  · refine le_antisymm ?_ ?_
+    · rw [le_iInf_iff]
+      rintro j s ⟨t, ht, rfl⟩
+      refine ⟨Homeomorph.ulift.symm ⁻¹' ((uliftFunctor.map (c.π.app j)) ⁻¹' t), ?_, rfl⟩
+      apply Homeomorph.ulift.continuous_invFun.isOpen_preimage
+      apply (uliftFunctor.map (c.π.app j)).hom.continuous_toFun.isOpen_preimage _ ht
+    · change _ ≤ TopologicalSpace.induced _ _
+      rw [← generateFrom_iUnion_isOpen, induced_of_isLimit _ hc, induced_iInf, le_iInf_iff]
+      rintro i s ⟨-, ⟨t, ht, rfl⟩, rfl⟩
+      refine .basic _ ?_
+      rw [Set.mem_iUnion]
+      exact ⟨i, ULift.down ⁻¹' t, Homeomorph.ulift.continuous_toFun.isOpen_preimage _ ht, rfl⟩
+  · exact isLimitOfPreserves (forget TopCat ⋙ CategoryTheory.uliftFunctor) hc
+
+instance : PreservesColimitsOfSize.{w', w} uliftFunctor.{v, u} := by
+  refine ⟨⟨fun {K} ↦ ⟨fun {c} hc ↦ ?_⟩⟩⟩
+  rw [nonempty_isColimit_iff_eq_coinduced]
+  · ext s
+    rw [Homeomorph.ulift.symm.isOpenEmbedding.isOpen_iff_preimage_isOpen (by simp),
+      isOpen_iff_of_isColimit _ hc, isOpen_iSup_iff]
+    congr!
+    rw [Homeomorph.ulift.isOpenEmbedding.isOpen_iff_preimage_isOpen (by simp)]
+    rfl
+  · exact isColimitOfPreserves (forget TopCat ⋙ CategoryTheory.uliftFunctor) hc
+
 end TopCat