feat: homeomorphism between C(X, Σ i, Y i) and Σ i, C(X, Y i) (#5673)

This is a follow-up to #4325.

Author: urkud

Mathlib.lean

@@ -3142,6 +3142,7 @@ import Mathlib.Topology.ContinuousFunction.Ideals
 import Mathlib.Topology.ContinuousFunction.LocallyConstant
 import Mathlib.Topology.ContinuousFunction.Ordered
 import Mathlib.Topology.ContinuousFunction.Polynomial
+import Mathlib.Topology.ContinuousFunction.Sigma
 import Mathlib.Topology.ContinuousFunction.StoneWeierstrass
 import Mathlib.Topology.ContinuousFunction.T0Sierpinski
 import Mathlib.Topology.ContinuousFunction.Units

Mathlib/Topology/CompactOpen.lean

@@ -132,7 +132,6 @@ private theorem image_gen {s : Set α} (_ : IsCompact s) {u : Set γ} (_ : IsOpe
   ext ⟨g, _⟩
   change g ∘ f '' s ⊆ u ↔ g '' (f '' s) ⊆ u
   rw [Set.image_comp]
---#align continuous_map.image_gen continuous_map.image_gen
 
 /-- C(-, γ) is a functor. -/
 theorem continuous_comp_left : Continuous (fun g => g.comp f : C(β, γ) → C(α, γ)) :=

Mathlib/Topology/Constructions.lean

@@ -1533,6 +1533,22 @@ theorem continuous_sigma {f : Sigma σ → α} (hf : ∀ i, Continuous fun a =>
   continuous_sigma_iff.2 hf
 #align continuous_sigma continuous_sigma
 
+/-- A map defined on a sigma type (a.k.a. the disjoint union of an indexed family of topological
+spaces) is inducing iff its restriction to each component is inducing and each the image of each
+component under `f` can be separated from the images of all other components by an open set. -/
+theorem inducing_sigma {f : Sigma σ → α} :
+    Inducing f ↔ (∀ i, Inducing (f ∘ Sigma.mk i)) ∧
+      (∀ i, ∃ U, IsOpen U ∧ ∀ x, f x ∈ U ↔ x.1 = i) := by
+  refine ⟨fun h ↦ ⟨fun i ↦ h.comp embedding_sigmaMk.1, fun i ↦ ?_⟩, ?_⟩
+  · rcases h.isOpen_iff.1 (isOpen_range_sigmaMk (i := i)) with ⟨U, hUo, hU⟩
+    refine ⟨U, hUo, ?_⟩
+    simpa [Set.ext_iff] using hU
+  · refine fun ⟨h₁, h₂⟩ ↦ inducing_iff_nhds.2 fun ⟨i, x⟩ ↦ ?_
+    rw [Sigma.nhds_mk, (h₁ i).nhds_eq_comap, comp_apply, ← comap_comap, map_comap_of_mem]
+    rcases h₂ i with ⟨U, hUo, hU⟩
+    filter_upwards [preimage_mem_comap <| hUo.mem_nhds <| (hU _).2 rfl] with y hy
+    simpa [hU] using hy
+
 @[simp 1100]
 theorem continuous_sigma_map {f₁ : ι → κ} {f₂ : ∀ i, σ i → τ (f₁ i)} :
     Continuous (Sigma.map f₁ f₂) ↔ ∀ i, Continuous (f₂ i) :=

Mathlib/Topology/ContinuousFunction/Basic.lean

@@ -324,6 +324,12 @@ def prodSwap : C(α × β, β × α) := .prodMk .snd .fst
 
 end Prod
 
+/-- `Sigma.mk i` as a bundled continuous map. -/
+@[simps apply]
+def sigmaMk {ι : Type _} {Y : ι → Type _} [∀ i, TopologicalSpace (Y i)] (i : ι) :
+    C(Y i, Σ i, Y i) where
+  toFun := Sigma.mk i
+
 section Pi
 
 variable {I A : Type _} {X Y : I → Type _} [TopologicalSpace A] [∀ i, TopologicalSpace (X i)]

Mathlib/Topology/ContinuousFunction/Sigma.lean

@@ -0,0 +1,82 @@
+/-
+Copyright (c) 2023 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Topology.Connected
+import Mathlib.Topology.CompactOpen
+
+/-!
+# Equivalence between `C(X, Σ i, Y i)` and `Σ i, C(X, Y i)`
+
+If `X` is a connected topological space, then for every continuous map `f` from `X` to the disjoint
+union of a collection of topological spaces `Y i` there exists a unique index `i` and a continuous
+map from `g` to `Y i` such that `f` is the composition of the natural embedding
+`Sigma.mk i : Y i → Σ i, Y i` with `g`.
+
+This defines an equivalence between `C(X, Σ i, Y i)` and `Σ i, C(X, Y i)`. In fact, this equivalence
+is a homeomorphism if the spaces of continuous maps are equipped with the compact-open topology.
+
+## Implementation notes
+
+There are two natural ways to talk about this result: one is to say that for each `f` there exist
+unique `i` and `g`; another one is to define a noncomputable equivalence. We choose the second way
+because it is easier to use an equivalence in applications.
+
+## TODO
+
+Some results in this file can be generalized to the case when `X` is a preconnected space. However,
+if `X` is empty, then any index `i` will work, so there is no 1-to-1 corespondence.
+
+## Keywords
+
+continuous map, sigma type, disjoint union
+-/
+
+noncomputable section
+
+open scoped Topology
+open Filter
+
+variable {X ι : Type _} {Y : ι → Type _} [TopologicalSpace X] [∀ i, TopologicalSpace (Y i)]
+
+namespace ContinuousMap
+
+theorem embedding_sigmaMk_comp [Nonempty X] :
+    Embedding (fun g : Σ i, C(X, Y i) ↦ (sigmaMk g.1).comp g.2) where
+  toInducing := inducing_sigma.2
+    ⟨fun i ↦ (sigmaMk i).inducing_comp embedding_sigmaMk.toInducing, fun i ↦
+      let ⟨x⟩ := ‹Nonempty X›
+      ⟨_, (isOpen_sigma_fst_preimage {i}).preimage (continuous_eval_const x), fun _ ↦ Iff.rfl⟩⟩
+  inj := by
+    · rintro ⟨i, g⟩ ⟨i', g'⟩ h
+      obtain ⟨rfl, hg⟩ : i = i' ∧ HEq (⇑g) (⇑g') :=
+        Function.eq_of_sigmaMk_comp <| congr_arg FunLike.coe h
+      simpa using hg
+
+section ConnectedSpace
+
+variable [ConnectedSpace X]
+
+/-- Every a continuous map from a connected topological space to the disjoint union of a family of
+topological spaces is a composition of the embedding `ContinuousMap.sigmMk i : C(Y i, Σ i, Y i)` for
+some `i` and a continuous map `g : C(X, Y i)`. See also `Continuous.exists_lift_sigma` for a version
+with unbundled functions and `ContinuousMap.sigmaCodHomeomorph` for a homeomorphism defined using
+this fact. -/
+theorem exists_lift_sigma (f : C(X, Σ i, Y i)) : ∃ i g, f = (sigmaMk i).comp g :=
+  let ⟨i, g, hg, hfg⟩ := f.continuous.exists_lift_sigma
+  ⟨i, ⟨g, hg⟩, FunLike.ext' hfg⟩
+
+variable (X Y)
+
+/-- Homeomorphism between the type `C(X, Σ i, Y i)` of continuous maps from a connected topological
+space to the disjoint union of a family of topological spaces and the disjoint union of the types of
+continuous maps `C(X, Y i)`.
+
+The inverse map sends `⟨i, g⟩` to `ContinuousMap.comp (ContinuousMap.sigmaMk i) g`. -/
+@[simps! symm_apply]
+def sigmaCodHomeomorph : C(X, Σ i, Y i) ≃ₜ Σ i, C(X, Y i) :=
+  .symm <| Equiv.toHomeomorphOfInducing
+    (.ofBijective _ ⟨embedding_sigmaMk_comp.inj, fun f ↦
+      let ⟨i, g, hg⟩ := f.exists_lift_sigma; ⟨⟨i, g⟩, hg.symm⟩⟩)
+    embedding_sigmaMk_comp.toInducing