# 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

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.

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