Covering spaces of a disjoint union are classified by their monodromy

Let X i be a family of path-connected, locally path-connected, semilocally simply connected spaces. Their disjoint union is locally path connected but not path connected, so it falls outside the standing hypotheses of TauCeti.CoveringSpace.monodromyEquivalence; this file proves the classification for it anyway.

Only essential surjectivity has to be redone: monodromy is always faithful, and it is full over any locally path-connected base. A functor F out of the fundamental groupoid of Σ i, X i restricts along the inclusion of each summand, each restriction is the monodromy of a covering space of that summand, and the disjoint union of those covering spaces is a covering space of Σ i, X i whose monodromy is F. The comparison is natural because a path in a disjoint union stays in the summand it starts in, so every morphism of the fundamental groupoid comes from a single summand.

Main declarations

• TauCeti.sigmaMonodromyNatIso: summandwise identifications of monodromy assemble into one over the disjoint union.
• TauCeti.CoveringSpace.exists_monodromyFunctor_iso_sigma: every functor out of the fundamental groupoid of a disjoint union is the monodromy of a covering space.
• TauCeti.CoveringSpace.sigmaMonodromyEquivalence: covering spaces of a disjoint union of nice spaces are equivalent to functors from its fundamental groupoid to types.

References

This is the disconnected case of Stage 2, item 8 of TauCetiRoadmap/UniversalCovers/README.md, whose alternative lens asks for covers in general to be described as functors out of the fundamental groupoid.

noncomputable def TauCeti.sigmaMonodromyNatIso {ι : Type u} {E X : ι → Type u} [(i : ι) → TopologicalSpace (E i)] [(i : ι) → TopologicalSpace (X i)] (f : (i : ι) → E i → X i) (hf : ∀ (i : ι), IsCoveringMap (f i)) (G : CategoryTheory.Functor (FundamentalGroupoid ((i : ι) × X i)) (Type u)) (e : (i : ι) → ⋯.monodromyFunctor ≅ (FundamentalGroupoid.map { toFun := Sigma.mk i, continuous_toFun := ⋯ }).comp G) : ⋯.monodromyFunctor ≅ G

Summandwise identifications of monodromy assemble over a disjoint union. If the monodromy functor of f i is isomorphic to the restriction of G to the i-th summand for every i, then the monodromy functor of the disjoint union of the f i is isomorphic to G.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.CoveringSpace.exists_monodromyFunctor_iso_sigma {ι : Type u} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), PathConnectedSpace (X i)] [∀ (i : ι), LocallyPathConnectedSpace (X i)] [∀ (i : ι), SemilocallySimplyConnectedSpace (X i)] (F : CategoryTheory.Functor (FundamentalGroupoid ((i : ι) × X i)) (Type u)) : ∃ (p : CoveringSpace ↧((i : ι) × X i)), Nonempty ((monodromyFunctor ↧((i : ι) × X i)).obj p ≅ F)

Every functor out of the fundamental groupoid of a disjoint union of nice spaces is the monodromy of a covering space.

noncomputable def TauCeti.CoveringSpace.sigmaMonodromyEquivalence {ι : Type u} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), PathConnectedSpace (X i)] [∀ (i : ι), LocallyPathConnectedSpace (X i)] [∀ (i : ι), SemilocallySimplyConnectedSpace (X i)] : CoveringSpace ↧((i : ι) × X i) ≌ CategoryTheory.Functor (FundamentalGroupoid ((i : ι) × X i)) (Type u)

The classification of covering spaces of a disjoint union by fundamental-groupoid actions. Over a disjoint union of path-connected, locally path-connected, semilocally simply connected spaces, monodromy is an equivalence from covering spaces to functors from the fundamental groupoid to types.

Equations

• TauCeti.CoveringSpace.sigmaMonodromyEquivalence X = (TauCeti.CoveringSpace.monodromyFunctor ↧((i : ι) × X i)).asEquivalence

@[simp]

theorem TauCeti.CoveringSpace.sigmaMonodromyEquivalence_functor {ι : Type u} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), PathConnectedSpace (X i)] [∀ (i : ι), LocallyPathConnectedSpace (X i)] [∀ (i : ι), SemilocallySimplyConnectedSpace (X i)] : (sigmaMonodromyEquivalence X).functor = monodromyFunctor ↧((i : ι) × X i)