Retracting a disjoint union onto a summand

For a point z of the summand Z i of a disjoint union Σ j, Z j, the continuous map ContinuousMap.sigmaRetraction i z is the identity on Z i and sends every other summand to z. It is a retraction of the inclusion ContinuousMap.sigmaMk i (ContinuousMap.sigmaRetraction_comp_sigmaMk).

Main definitions

• ContinuousMap.sigmaRetraction i z: the retraction of Σ j, Z j onto Z i collapsing the other summands to z.

noncomputable def ContinuousMap.sigmaRetraction {ι : Type u_1} {Z : ι → Type u_2} [(i : ι) → TopologicalSpace (Z i)] (i : ι) (z : Z i) : C((j : ι) × Z j, Z i)

The retraction of a disjoint union onto its summand Z i, sending every other summand to the point z.

@[simp]

theorem ContinuousMap.sigmaRetraction_sigmaMk {ι : Type u_1} {Z : ι → Type u_2} [(i : ι) → TopologicalSpace (Z i)] (i : ι) (z w : Z i) : (sigmaRetraction i z) ⟨i, w⟩ = w

@[simp]

theorem ContinuousMap.sigmaRetraction_apply_of_ne {ι : Type u_1} {Z : ι → Type u_2} [(i : ι) → TopologicalSpace (Z i)] {i j : ι} (z : Z i) (w : Z j) (h : j ≠ i) : (sigmaRetraction i z) ⟨j, w⟩ = z

@[simp]

theorem ContinuousMap.sigmaRetraction_comp_sigmaMk {ι : Type u_1} {Z : ι → Type u_2} [(i : ι) → TopologicalSpace (Z i)] (i : ι) (z : Z i) : (sigmaRetraction i z).comp (sigmaMk i) = ContinuousMap.id (Z i)