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 correspondence.

Keywords

continuous map, sigma type, disjoint union

theorem ContinuousMap.embedding_sigmaMk_comp {X : Type u_1} {ι : Type u_2} {Y : ι → Type u_3} [TopologicalSpace X] [(i : ι) → TopologicalSpace (Y i)] [Nonempty X] : Embedding fun (g : (i : ι) × C(X, Y i)) => (ContinuousMap.sigmaMk g.fst).comp g.snd

theorem ContinuousMap.exists_lift_sigma {X : Type u_1} {ι : Type u_2} {Y : ι → Type u_3} [TopologicalSpace X] [(i : ι) → TopologicalSpace (Y i)] [ConnectedSpace X] (f : C(X, (i : ι) × Y i)) : ∃ (i : ι) (g : C(X, Y i)), f = (ContinuousMap.sigmaMk i).comp g

Every 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.

@[simp]

theorem ContinuousMap.sigmaCodHomeomorph_symm_apply (X : Type u_1) {ι : Type u_2} (Y : ι → Type u_3) [TopologicalSpace X] [(i : ι) → TopologicalSpace (Y i)] [ConnectedSpace X] : ∀ (a : (i : ι) × C(X, Y i)), (ContinuousMap.sigmaCodHomeomorph X Y).symm a = (ContinuousMap.sigmaMk a.fst).comp a.snd

def ContinuousMap.sigmaCodHomeomorph (X : Type u_1) {ι : Type u_2} (Y : ι → Type u_3) [TopologicalSpace X] [(i : ι) → TopologicalSpace (Y i)] [ConnectedSpace X] : C(X, (i : ι) × Y i) ≃ₜ (i : ι) × C(X, Y i)

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.

Equations

• ContinuousMap.sigmaCodHomeomorph X Y = ((Equiv.ofBijective (fun (g : (i : ι) × C(X, Y i)) => (ContinuousMap.sigmaMk g.fst).comp g.snd) ⋯).toHomeomorphOfInducing ⋯).symm