Connected covering spaces are the categorically connected ones

Let X be path connected, locally path connected and semilocally simply connected. Covering spaces of X carry two unrelated-looking notions of connectedness: the topological one, that the total space is a ConnectedSpace, and the categorical one, CategoryTheory.PreGaloisCategory.IsConnected, which asks that the cover is not an initial object of TauCeti.CoveringSpace X and has no nontrivial subobject there. This file proves that they agree.

The bridge is the classification of covers by π₁(X, x₀)-sets. Categorical connectedness is invariant under an equivalence of categories (TauCeti.isConnected_map_iff), so it can be read off on the other side of TauCeti.CoveringSpace.fiberActionEquivalence, where it says exactly that the monodromy action on the fibre over x₀ is transitive and nonempty (TauCeti.isConnected_action_iff_isTransitiveAction). That in turn is the condition already known to characterise connected covers: transitivity of monodromy is TauCeti.ConnectedCoveringSpace.isTransitiveAction_fiberAction, and conversely a cover with transitive monodromy has path-connected total space, because path lifting joins every point of the total space to a point of the fibre over x₀ and monodromy joins any two points of that fibre. That converse needs no hypothesis on X beyond path connectedness, so the dictionary between transitive monodromy and a connected total space is established before the classification is invoked; only the passage to the categorical statement uses the full standing hypotheses.

The initial objects of TauCeti.CoveringSpace X play no special role here: they are the covers with empty total space over any base, which is TauCeti.CoveringSpace.isInitial_iff_isEmpty in the general covering-space API.

Main declarations

• TauCeti.CoveringSpace.isTransitiveAction_fiberAction_iff_connectedSpace: the monodromy action on the fibre over x₀ is transitive exactly when the total space is connected.
• TauCeti.CoveringSpace.isConnected_iff_connectedSpace: a covering space of X is a connected object of TauCeti.CoveringSpace X exactly when its total space is a connected space.
• TauCeti.ConnectedCoveringSpace.isConnected_forget_obj: a connected covering space is a connected object of TauCeti.CoveringSpace X.

References

This is the connectedness dictionary for the alternative lens of Stage 2, item 8 of TauCetiRoadmap/UniversalCovers/README.md. It consumes the classification of covers by π₁(X, x₀)-sets and Mathlib's CategoryTheory.PreGaloisCategory.IsConnected; no Mathlib proof is vendored.

theorem TauCeti.CoveringSpace.isTransitiveAction_fiberAction_iff_connectedSpace {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] (p : CoveringSpace X) : isTransitiveAction (FundamentalGroup (↑X) x₀) ((fiberActionFunctor x₀).obj p) ↔ ConnectedSpace ↑p.obj.left

The monodromy action of π₁(X, x₀) on the fibre of a covering space over x₀ is transitive exactly when the total space of that cover is connected.

This is deliberately not @[simp]: TauCeti.isTransitiveAction_iff is already a simp lemma, so the left-hand side is not in simp normal form and simpNF rejects the attribute.

@[simp]

theorem TauCeti.CoveringSpace.isConnected_iff_connectedSpace {X : TopCat} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] (p : CoveringSpace X) : CategoryTheory.PreGaloisCategory.IsConnected p ↔ ConnectedSpace ↑p.obj.left

A covering space of X is a connected object of TauCeti.CoveringSpace X exactly when its total space is a connected space.

theorem TauCeti.ConnectedCoveringSpace.isConnected_forget_obj {X : TopCat} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] (p : ConnectedCoveringSpace X) : CategoryTheory.PreGaloisCategory.IsConnected ((forget X).obj p)

A connected covering space is a connected object of TauCeti.CoveringSpace X.