The algebraic topology of a path component

Loops and path homotopies based in pathComponent x₀ remain there. Consequently, when the ambient space is semilocally simply connected, the path component inherits semilocal simple connectivity, and its inclusion into the ambient space induces an isomorphism on fundamental groups at every point of the component.

Main declarations

• An instance making ↥(pathComponent x₀) semilocally simply connected.
• FundamentalGroup.pathComponentMulEquiv: the inclusion of pathComponent x₀ induces an isomorphism of fundamental groups at any point of the component.
• FundamentalGroup.pathComponentMulEquiv_symm_fromPath: the inverse corestricts a loop to its path component.

References

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

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

A path component inherits semilocal simple connectivity: an ambient null-homotopy based in the component remains in that component.

instance TauCeti.instSemilocallySimplyConnectedSpaceConnectedComponentsFiber {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (C : ConnectedComponents X) : SemilocallySimplyConnectedSpace ↑(ConnectedComponents.mk ⁻¹' {C})

A fibre of the quotient to connected components is semilocally simply connected when the ambient space is locally path-connected and semilocally simply connected.

noncomputable def FundamentalGroup.pathComponentMulEquiv {X : Type u_1} [TopologicalSpace X] (x₀ : X) (a : ↑(pathComponent x₀)) : FundamentalGroup (↑(pathComponent x₀)) a ≃* FundamentalGroup X ↑a

The path component of x₀ carries the ambient fundamental group at each of its points. Loops at such a point and their homotopies never leave the path component.

Equations

• FundamentalGroup.pathComponentMulEquiv x₀ a = MulEquiv.ofBijective (FundamentalGroup.map { toFun := Subtype.val, continuous_toFun := ⋯ } a) ⋯

@[simp]

theorem FundamentalGroup.pathComponentMulEquiv_apply {X : Type u_1} [TopologicalSpace X] (x₀ : X) (a : ↑(pathComponent x₀)) (g : FundamentalGroup (↑(pathComponent x₀)) a) : (pathComponentMulEquiv x₀ a) g = (map { toFun := Subtype.val, continuous_toFun := ⋯ } a) g

@[simp]

theorem FundamentalGroup.pathComponentMulEquiv_symm_fromPath {X : Type u_1} [TopologicalSpace X] (x₀ : X) (a : ↑(pathComponent x₀)) (γ : Path ↑a ↑a) : (pathComponentMulEquiv x₀ a).symm (fromPath (Path.Homotopic.Quotient.mk γ)) = fromPath (Path.Homotopic.Quotient.mk (γ.codRestrict ⋯))

The inverse path-component equivalence corestricts a representative loop to the path component containing its basepoint.