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
Alias of ContinuousMap.isEmbedding_sigmaMk_comp.
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) ⋯).toHomeomorphOfIsInducing ⋯).symm