From 92d4b01aea279509d867744b54e70a37ff243af9 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 17 Dec 2023 15:16:28 +0000
Subject: [PATCH] feat: add topological lemmas for `ULift` (#8958)

This also adds a handful of easy instances

Arguably the topological space instance should be defined via `coinduced` to make these true by `Iff.rfl`, but that creates a headache with constructors for normed spaces, so is not in this PR.
---
 .../FundamentalGroupoid/InducedMaps.lean       |  2 +-
 Mathlib/Topology/Constructions.lean            | 10 ++++++++++
 Mathlib/Topology/Separation.lean               | 18 ++++++++++++++++++
 3 files changed, 29 insertions(+), 1 deletion(-)

diff --git a/Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean b/Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean
index fdb14960f8315..b4d70283c0093 100644
--- a/Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean
+++ b/Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean
@@ -142,7 +142,7 @@ many of the paths do not have defeq starting/ending points, so we end up needing
 /-- Interpret a homotopy `H : C(I × X, Y)` as a map `C(ULift I × X, Y)` -/
 def uliftMap : C(TopCat.of (ULift.{u} I × X), Y) :=
   ⟨fun x => H (x.1.down, x.2),
-    H.continuous.comp ((continuous_induced_dom.comp continuous_fst).prod_mk continuous_snd)⟩
+    H.continuous.comp ((continuous_uLift_down.comp continuous_fst).prod_mk continuous_snd)⟩
 #align continuous_map.homotopy.ulift_map ContinuousMap.Homotopy.uliftMap
 
 -- This lemma has always been bad, but the linter only noticed after lean4#2644.
diff --git a/Mathlib/Topology/Constructions.lean b/Mathlib/Topology/Constructions.lean
index 5ce81050e5fba..e681390b4ad7e 100644
--- a/Mathlib/Topology/Constructions.lean
+++ b/Mathlib/Topology/Constructions.lean
@@ -1650,6 +1650,16 @@ end Sigma
 
 section ULift
 
+theorem ULift.isOpen_iff [TopologicalSpace α] {s : Set (ULift.{v} α)} :
+    IsOpen s ↔ IsOpen (ULift.up ⁻¹' s) := by
+  unfold ULift.topologicalSpace
+  erw [← Equiv.ulift.coinduced_symm]
+  rfl
+
+theorem ULift.isClosed_iff [TopologicalSpace α] {s : Set (ULift.{v} α)} :
+    IsClosed s ↔ IsClosed (ULift.up ⁻¹' s) := by
+  rw [← isOpen_compl_iff, ← isOpen_compl_iff, isOpen_iff, preimage_compl]
+
 @[continuity]
 theorem continuous_uLift_down [TopologicalSpace α] : Continuous (ULift.down : ULift.{v, u} α → α) :=
   continuous_induced_dom
diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean
index bccc397e77bd7..d828fd9ce59af 100644
--- a/Mathlib/Topology/Separation.lean
+++ b/Mathlib/Topology/Separation.lean
@@ -362,6 +362,9 @@ instance Pi.instT0Space {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace
   ⟨fun _ _ h => funext fun i => (h.map (continuous_apply i)).eq⟩
 #align pi.t0_space Pi.instT0Space
 
+instance ULift.instT0Space [T0Space X] : T0Space (ULift X) :=
+  embedding_uLift_down.t0Space
+
 theorem T0Space.of_cover (h : ∀ x y, Inseparable x y → ∃ s : Set X, x ∈ s ∧ y ∈ s ∧ T0Space s) :
     T0Space X := by
   refine' ⟨fun x y hxy => _⟩
@@ -627,6 +630,9 @@ instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i,
     T1Space (∀ i, X i) :=
   ⟨fun f => univ_pi_singleton f ▸ isClosed_set_pi fun _ _ => isClosed_singleton⟩
 
+instance ULift.instT1Space [T1Space X] : T1Space (ULift X) :=
+  embedding_uLift_down.t1Space
+
 -- see Note [lower instance priority]
 instance (priority := 100) T1Space.t0Space [T1Space X] : T0Space X :=
   ⟨fun _ _ h => h.specializes.eq⟩
@@ -1234,6 +1240,9 @@ theorem Embedding.t2Space [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : E
   .of_injective_continuous hf.inj hf.continuous
 #align embedding.t2_space Embedding.t2Space
 
+instance ULift.instT2Space [T2Space X] : T2Space (ULift X) :=
+  embedding_uLift_down.t2Space
+
 instance [T2Space X] [TopologicalSpace Y] [T2Space Y] :
     T2Space (X ⊕ Y) := by
   constructor
@@ -1837,6 +1846,9 @@ instance Subtype.t3Space [T3Space X] {p : X → Prop} : T3Space (Subtype p) :=
   embedding_subtype_val.t3Space
 #align subtype.t3_space Subtype.t3Space
 
+instance ULift.instT3Space [T3Space X] : T3Space (ULift X) :=
+  embedding_uLift_down.t3Space
+
 instance [TopologicalSpace Y] [T3Space X] [T3Space Y] : T3Space (X × Y) := ⟨⟩
 
 instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, T3Space (X i)] :
@@ -1974,6 +1986,9 @@ protected theorem ClosedEmbedding.t4Space [TopologicalSpace Y] [T4Space Y] {f :
   toNormalSpace := hf.normalSpace
 #align closed_embedding.normal_space ClosedEmbedding.t4Space
 
+instance ULift.instT4Space [T4Space X] : T4Space (ULift X) :=
+  ULift.closedEmbedding_down.t4Space
+
 namespace SeparationQuotient
 
 /-- The `SeparationQuotient` of a normal space is a normal space. -/
@@ -2020,6 +2035,9 @@ theorem Embedding.t5Space [TopologicalSpace Y] [T5Space Y] {e : X → Y} (he : E
 instance [T5Space X] {p : X → Prop} : T5Space { x // p x } :=
   embedding_subtype_val.t5Space
 
+instance ULift.instT5Space [T5Space X] : T5Space (ULift X) :=
+  embedding_uLift_down.t5Space
+
 -- see Note [lower instance priority]
 /-- A `T₅` space is a `T₄` space. -/
 instance (priority := 100) T5Space.toT4Space [T5Space X] : T4Space X where