feat (Topology.IsQuotientMap) : quotient maps for Sum.map, Sigma.map, sigma of coherent subspaces

Author: robertmaxton42

Mathlib/Topology/Coherent.lean

@@ -5,6 +5,7 @@ Authors: Yury Kudryashov
 -/
 import Mathlib.Topology.Defs.Sequences
 import Mathlib.Topology.ContinuousOn
+import Mathlib.Topology.ContinuousMap.Basic
 
 /-!
 # Topology generated by its restrictions to subsets
@@ -32,7 +33,8 @@ and provide the others as corollaries.
 
 open Filter Set
 
-variable {X : Type*} [TopologicalSpace X] {S : Set (Set X)} {t : Set X} {x : X}
+variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
+  {S : Set (Set X)} {t : Set X} {x : X}
 
 namespace Topology.IsCoherentWith
 
@@ -90,4 +92,27 @@ lemma of_nhds (h : ∀ x, ∃ s ∈ S, s ∈ 𝓝 x) : IsCoherentWith S :=
     let ⟨s, hsS, hsx⟩ := h x
     (hf s hsS).continuousAt hsx
 
+/-- If a space `X` is coherent with an indexed family of subspaces `S` whose union is `X`, then the
+ canonical inclusion from `Σ i, S i` to `X` is a quotient map. -/
+lemma isQuotientMap_sigma_desc'
+    {ι : Type*} {S : ι → Set X} (hX : IsCoherentWith (range S)) (hS : ⋃ i, S i = univ) :
+    IsQuotientMap (ContinuousMap.sigma (fun _ ↦ ContinuousMap.subtypeVal) : C(Σ i, S i, X)) where
+  surjective y := by
+    rw [iUnion_eq_univ_iff] at hS
+    obtain ⟨i, hx⟩ := hS y
+    use Sigma.mk i ⟨y, hx⟩
+    simp
+  eq_coinduced := by
+    ext t
+    unfold instTopologicalSpaceSigma
+    simp [hX.isOpen_iff (t := t), isOpen_coinduced, isOpen_iSup_iff, preimage_preimage]
+
+/-- If a space `X` is coherent with a set of subspaces `S` whose union is `X`, then the
+ canonical inclusion from `Σ i, S i` to `X` is a quotient map. -/
+lemma isQuotientMap_sigma_desc (hX : IsCoherentWith S) (hS : ⋃₀ S = univ) :
+    IsQuotientMap (ContinuousMap.sigma (fun _ ↦ ContinuousMap.subtypeVal) : C(Σ (s : S), s, X)) :=
+  have h : S = range Subtype.val := by simp
+  IsCoherentWith.isQuotientMap_sigma_desc' (S := ((↑) : S → Set X))
+    (h ▸ hX) (sUnion_eq_iUnion ▸ hS)
+
 end Topology.IsCoherentWith

Mathlib/Topology/Constructions.lean

@@ -1184,6 +1184,22 @@ lemma Topology.isOpenEmbedding_sigmaMap {f₁ : ι → κ} {f₂ : ∀ i, σ i 
   simp only [isOpenEmbedding_iff_isEmbedding_isOpenMap, isOpenMap_sigma_map, isEmbedding_sigmaMap h,
     forall_and]
 
+lemma Topology.IsQuotientMap.sigmaMap {f₁ : ι → κ} {f₂ : (i : ι) → σ i → τ (f₁ i)}
+    (h₁ : f₁.Surjective) (h₂ : ∀ i, IsQuotientMap (f₂ i)) :
+    IsQuotientMap (Sigma.map f₁ f₂) := by
+  fconstructor
+  · rintro ⟨k, t⟩
+    obtain ⟨i, rfl⟩ := h₁ k
+    obtain ⟨s, rfl⟩ := (h₂ i).surjective t
+    use ⟨i, s⟩
+    simp [Sigma.map]
+  · simp_rw [instTopologicalSpaceSigma, coinduced_iSup, coinduced_compose, Function.comp_def,
+    Sigma.map_mk, ← Function.comp_def, ← coinduced_compose, ← (h₂ · |>.eq_coinduced)]
+    conv_lhs => enter [1, k]
+    rw [← range_eq_univ] at h₁
+    rw [← iSup_univ (β := ι), ← iSup_image (g := (fun k ↦ coinduced (Sigma.mk k) _))]
+    simp_rw [image_univ, h₁, iSup_univ]
+
 end Sigma
 
 section ULift

Mathlib/Topology/Constructions/SumProd.lean

@@ -844,6 +844,18 @@ lemma IsClosedEmbedding.sumElim {f : X → Z} {g : Y → Z}
   rw [IsClosedEmbedding.isClosedEmbedding_iff_continuous_injective_isClosedMap] at hf hg ⊢
   exact ⟨hf.1.sumElim hg.1, h, hf.2.2.sumElim hg.2.2⟩
 
+lemma IsQuotientMap.sumMap (f : X → Y) (g : Z → W) (h₁ : IsQuotientMap f) (h₂ : IsQuotientMap g) :
+    IsQuotientMap (Sum.map f g) := by
+  fconstructor
+  · rintro (x | y)
+    · use .inl (h₁.surjective x).choose
+      simp [h₁.surjective x |>.choose_spec]
+    · use .inr (h₂.surjective y).choose
+      simp [h₂.surjective y |>.choose_spec]
+  · simp_rw [instTopologicalSpaceSum, coinduced_sup, coinduced_compose, Function.comp_def,
+    Sum.map_inl, Sum.map_inr, ← Function.comp_def, ← coinduced_compose, h₁.eq_coinduced,
+    h₂.eq_coinduced]
+
 -- Homeomorphisms between the various constructions: sums of two homeomorphisms,
 -- as well as commutativity, associativity and distributivity with products.
 namespace Homeomorph

Mathlib/Topology/ContinuousMap/Basic.lean

@@ -612,6 +612,13 @@ theorem lift_comp : (hf.lift g h).comp f = g := by
   ext
   simpa using h (Function.rightInverse_surjInv _ _)
 
+@[simp↓]
+lemma lift_comp_apply {X Y Z : Type*} [TopologicalSpace X]
+    [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} (hf : IsQuotientMap f)
+    (g : C(X, Z)) (hg : Function.FactorsThrough g f) (x : X) :
+    (hf.lift g hg) (f x) = g x := by
+  rw [← (hf.lift g hg).comp_apply, lift_comp]
+
 /-- `IsQuotientMap.lift` as an equivalence. -/
 @[simps]
 noncomputable def liftEquiv : { g : C(X, Z) // Function.FactorsThrough g f} ≃ C(Y, Z) where
@@ -623,6 +630,12 @@ noncomputable def liftEquiv : { g : C(X, Z) // Function.FactorsThrough g f} ≃
     ext a
     simpa using congrArg g (Function.rightInverse_surjInv hf.surjective a)
 
+/-- A version of `liftEquiv_apply` that is more convenient when rewriting. -/
+lemma liftEquiv_apply' {X Y Z : Type*} [TopologicalSpace X]
+    [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} (hf : IsQuotientMap f)
+    (g : C(X, Z)) (hg : Function.FactorsThrough g f) : hf.lift g hg =  hf.liftEquiv ⟨g, hg⟩ := by
+  rfl
+
 end Topology.IsQuotientMap
 end Lift