Point-set topology of path components

Paths and path homotopies based in pathComponent x₀ remain in that component, without any local path-connectedness assumption. This gives path connectedness of the component as a subspace; under local path connectedness of the ambient space, openness of path components also gives local path connectedness of the subspace.

Main declarations

• TauCeti.homotopic_pathComponent_of_map_subtypeVal_homotopic: path homotopies reflect along the inclusion of a path component.
• Instances making ↥(pathComponent x₀) path connected and locally path connected.
• TauCeti.pathComponentSelf: a point viewed in its own path component.
• Joined.eq_of_totallyDisconnectedSpace and ZerothHomotopy.mk_injective_of_totallyDisconnectedSpace: in a totally disconnected space, the path components are the points.

References

This supplies point-set prerequisites for the "or one builds the cover of pathComponent x₀" clause in TauCetiRoadmap/UniversalCovers/README.md.

theorem TauCeti.homotopic_pathComponent_of_map_subtypeVal_homotopic {X : Type u_1} [TopologicalSpace X] (x₀ : X) {a b : ↑(pathComponent x₀)} {γ δ : Path a b} (h : (γ.map ⋯).Homotopic (δ.map ⋯)) : γ.Homotopic δ

Two paths in a path component which are homotopic in the ambient space are already homotopic in the path component.

instance TauCeti.instPathConnectedSpaceSubtypePathComponent {X : Type u_1} [TopologicalSpace X] (x₀ : X) : PathConnectedSpace ↑(pathComponent x₀)

The path component of a point, as a subspace, is path connected.

instance TauCeti.instLocallyPathConnectedSpaceSubtypePathComponent {X : Type u_1} [TopologicalSpace X] (x₀ : X) [LocallyPathConnectedSpace X] : LocallyPathConnectedSpace ↑(pathComponent x₀)

In a locally path connected space the path components are open, hence locally path connected as subspaces.

@[reducible, inline]

abbrev TauCeti.pathComponentSelf {X : Type u_1} [TopologicalSpace X] (x₀ : X) : ↑(pathComponent x₀)

The basepoint of X, viewed as a point of its own path component.

Equations

• TauCeti.pathComponentSelf x₀ = ⟨x₀, ⋯⟩

theorem Joined.eq_of_totallyDisconnectedSpace {X : Type u_1} [TopologicalSpace X] [TotallyDisconnectedSpace X] {x y : X} (h : Joined x y) : x = y

In a totally disconnected space, points joined by a path are equal.

theorem ZerothHomotopy.mk_injective_of_totallyDisconnectedSpace {X : Type u_1} [TopologicalSpace X] [TotallyDisconnectedSpace X] : Function.Injective mk

In a totally disconnected space, distinct points lie in distinct path components.