Covering spaces over a locally path-connected base

Let X be locally path-connected and semilocally simply connected, with no connectedness assumption. Its connected components are open and coincide with its path components, so TauCeti.connectedComponentsSigmaHomeomorph identifies X with the disjoint union of the fibres of X → ConnectedComponents X. Each summand satisfies the standing hypotheses for the universal-cover construction.

The disjoint-union classification in TauCeti.AlgebraicTopology.UniversalCover.Classification.Sigma therefore applies. Composing the resulting covering projection with the component homeomorphism gives a cover of X; monodromy is transported by IsCoveringMap.monodromyHomeomorphCompNatIso. This proves essential surjectivity over an arbitrary base. Fullness only needs local path-connectedness, and faithfulness has no hypothesis, so monodromy is an equivalence.

Main declarations

• TauCeti.CoveringSpace.exists_monodromyFunctor_iso_of_locallyPathConnectedSpace: every functor from the fundamental groupoid of X to types is the monodromy of a covering space.
• TauCeti.CoveringSpace.monodromyEquivalenceOfLocallyPathConnectedSpace: covering spaces over a locally path-connected, semilocally simply connected base are equivalent to functors from its fundamental groupoid to types.

References

This closes the disconnected-cover part of Stage 2, item 8 of TauCetiRoadmap/UniversalCovers/README.md. It consumes the based-path universal-cover construction adapted from Kim Morrison's mathlib4#38292, and the disjoint-union classification already built from it. The mathematical classification follows Hatcher, Algebraic Topology, Section 1.3; no external formalization is copied or adapted here.

theorem TauCeti.CoveringSpace.exists_monodromyFunctor_iso_of_locallyPathConnectedSpace {X : Type u} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (F : CategoryTheory.Functor (FundamentalGroupoid X) (Type u)) : ∃ (p : CoveringSpace ↧X), Nonempty ((monodromyFunctor ↧X).obj p ≅ F)

Every fundamental-groupoid action over a locally path-connected, semilocally simply connected base is the monodromy of a covering space. No connectedness hypothesis is imposed on the base.

noncomputable def TauCeti.CoveringSpace.monodromyEquivalenceOfLocallyPathConnectedSpace (X : Type u) [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] : CoveringSpace ↧X ≌ CategoryTheory.Functor (FundamentalGroupoid X) (Type u)

Classification of covering spaces over an arbitrary locally path-connected, semilocally simply connected base. Monodromy is an equivalence from covering spaces over X to functors from the fundamental groupoid of X to types.

Equations

• TauCeti.CoveringSpace.monodromyEquivalenceOfLocallyPathConnectedSpace X = (TauCeti.CoveringSpace.monodromyFunctor ↧X).asEquivalence

@[simp]

theorem TauCeti.CoveringSpace.monodromyEquivalenceOfLocallyPathConnectedSpace_functor (X : Type u) [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] : (monodromyEquivalenceOfLocallyPathConnectedSpace X).functor = monodromyFunctor ↧X