# Documentation

Mathlib.Topology.ContinuousFunction.Sigma

# 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

theorem ContinuousMap.embedding_sigmaMk_comp {X : Type u_1} {ι : Type u_2} {Y : ιType u_3} [] [(i : ι) → TopologicalSpace (Y i)] [] :
Embedding fun g => ContinuousMap.comp () g.snd
theorem ContinuousMap.exists_lift_sigma {X : Type u_1} {ι : Type u_2} {Y : ιType u_3} [] [(i : ι) → TopologicalSpace (Y i)] [] (f : C(X, (i : ι) × Y i)) :
i 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) [] [(i : ι) → TopologicalSpace (Y i)] [] :
∀ (a : (i : ι) × C(X, Y i)), = ContinuousMap.comp () a.snd
def ContinuousMap.sigmaCodHomeomorph (X : Type u_1) {ι : Type u_2} (Y : ιType u_3) [] [(i : ι) → TopologicalSpace (Y i)] [] :
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.

Instances For