Paths in a disjoint union

A path in a disjoint union Σ i, X i never leaves the summand it starts in, because the unit interval is connected: this is Mathlib's ContinuousMap.exists_lift_sigma. This file draws the two consequences that the fundamental groupoid of a disjoint union needs, namely that the endpoint of a path out of the i-th summand again lies in the i-th summand, and that a path between two points of the i-th summand is the image of a path in that summand — the latter also for path homotopy classes.

The inclusion of a summand is spelled out as the anonymous bundled map ⟨Sigma.mk i, continuous_sigmaMk⟩ rather than ContinuousMap.sigmaMk i, because only the former has an application that reduces definitionally, which the dependently typed rewrites downstream need.

Main declarations

• TauCeti.sigmaFst_eq_of_path: a path out of the i-th summand of a disjoint union ends in the i-th summand.
• TauCeti.exists_path_map_sigmaMk_eq: a path between two points of the i-th summand is the image of a path in that summand.
• TauCeti.exists_quotient_map_sigmaMk_eq: the same for path homotopy classes.

References

This supplies the fundamental-groupoid half of the disconnected case of Stage 2, item 8 of TauCetiRoadmap/UniversalCovers/README.md.

theorem TauCeti.sigmaFst_eq_of_path {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {i : ι} {x : X i} {z : (j : ι) × X j} (γ : Path ⟨i, x⟩ z) : z.fst = i

A path out of the i-th summand of a disjoint union ends in the i-th summand.

theorem TauCeti.exists_path_map_sigmaMk_eq {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {i : ι} {x y : X i} (γ : Path ⟨i, x⟩ ⟨i, y⟩) : ∃ (γ' : Path x y), γ'.map ⋯ = γ

A path between two points of the i-th summand of a disjoint union is the image of a path in that summand.

theorem TauCeti.exists_quotient_map_sigmaMk_eq {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {i : ι} {x y : X i} (γ : Path.Homotopic.Quotient ⟨i, x⟩ ⟨i, y⟩) : ∃ (γ' : Path.Homotopic.Quotient x y), γ'.map { toFun := Sigma.mk i, continuous_toFun := ⋯ } = γ

A path homotopy class between two points of the i-th summand of a disjoint union is the image of a class in that summand.

theorem TauCeti.sigmaFst_eq_of_quotient {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {i : ι} {x : X i} {z : (j : ι) × X j} (γ : Path.Homotopic.Quotient ⟨i, x⟩ z) : z.fst = i

A path homotopy class out of the i-th summand of a disjoint union ends in the i-th summand.