Covering spaces are classified by fundamental-group sets #
Let X be path connected, locally path connected and semilocally simply connected, and fix a
basepoint x₀. This file proves that taking the fibre over x₀ with its monodromy action is an
equivalence of categories
TauCeti.CoveringSpace.fiberActionEquivalence :
CoveringSpace X ≌ Action (Type u) (FundamentalGroup X x₀),
that is, covering spaces of X are the same thing as sets with an action of π₁(X, x₀). It
restricts to an equivalence
TauCeti.ConnectedCoveringSpace.transitiveFiberActionEquivalence :
ConnectedCoveringSpace X ≌ TransitiveAction (FundamentalGroup X x₀)
between connected covers and transitive π₁(X, x₀)-sets.
This is the basepoint-based form of the classification. The basepoint-free form is already
available: TauCeti.CoveringSpace.monodromyEquivalence identifies covering spaces with functors
out of the fundamental groupoid. Passing from one to the other is pure category theory, and it
is where the hypotheses on X are spent a second time: path connectedness makes the fundamental
groupoid connected, and a connected groupoid is equivalent to the one-object category of its
vertex group by TauCeti.Groupoid.singleObjEquivalence. Precomposing a fundamental-groupoid
action with that equivalence, and reading a functor out of a one-object category as an action
through Mathlib's CategoryTheory.Action.functorCategoryEquivalence, gives the statement above.
No ᵐᵒᵖ intervenes. The vertex group of the fundamental groupoid at x₀ is π₁(X, x₀), since
Mathlib defines the latter as End (FundamentalGroupoid.mk x₀), and the composition convention
of CategoryTheory.SingleObj is the one that matches CategoryTheory.End. The ᵐᵒᵖ in
TauCeti.UniversalCover.deckFundamentalGroupEquiv comes from comparing monodromy with deck
transformations, which is a different comparison and is unaffected.
The action recovered here is the monodromy action of Mathlib/Topology/Homotopy/Lifting.lean:
fiberActionFunctor_obj_ρ_apply and fiberActionFunctor_obj_mulAction record that the
categorical action on the fibre is IsCoveringMap.fundamentalGroupMulAction, and
fiberActionFunctor_map_hom records that a map of covers acts on fibres by restriction.
Main declarations #
TauCeti.CoveringSpace.fiberActionFunctor: the functor sending a covering space to the fibre overx₀with its monodromy action ofπ₁(X, x₀).TauCeti.CoveringSpace.fiberActionFunctor_obj_V,TauCeti.CoveringSpace.fiberActionFunctor_obj_ρ_apply,TauCeti.CoveringSpace.fiberActionFunctor_obj_mulActionandTauCeti.CoveringSpace.fiberActionFunctor_map_hom: its values.TauCeti.CoveringSpace.fiberActionFunctor_faithful,TauCeti.CoveringSpace.fiberActionFunctor_full: over a path-connected, locally path-connected base the functor is fully faithful, without semilocal simple connectivity.TauCeti.CoveringSpace.fiberActionEquivalence: covering spaces ofXare equivalent toπ₁(X, x₀)-sets.TauCeti.ConnectedCoveringSpace.isTransitiveAction_fiberAction: theπ₁(X, x₀)-set attached to a connected cover is transitive, so the fibre-action functor restricts to a functorTauCeti.ConnectedCoveringSpace.transitiveFiberActionFunctorintoTauCeti.TransitiveAction (FundamentalGroup X x₀), with values given bytransitiveFiberActionFunctor_obj_objandtransitiveFiberActionFunctor_map_hom.TauCeti.ConnectedCoveringSpace.exists_fiberAction_iso: every transitiveπ₁(X, x₀)-set is the fibre action of a connected cover.TauCeti.ConnectedCoveringSpace.transitiveFiberActionEquivalence: connected covering spaces ofXare equivalent to transitiveπ₁(X, x₀)-sets.
References #
This is the π₁(X)-set form of the alternative lens on Stage 2, item 8 of
TauCetiRoadmap/UniversalCovers/README.md, which asks to "phrase the classification of
connected covers via transitive π₁(X)-sets / the monodromy functor, with disconnected covers
as functors out of the fundamental groupoid"; see Hatcher, Algebraic Topology, Section 1.3. It
consumes the fundamental-groupoid classification of
TauCeti.AlgebraicTopology.UniversalCover.Classification.MonodromyEquivalence, the
stabiliser-cover reconstruction of
TauCeti.AlgebraicTopology.UniversalCover.Classification.Reconstruction, which rests on the
based-path universal cover adapted from Kim Morrison's
mathlib4#38292, and Mathlib's
CategoryTheory.Action.functorCategoryEquivalence; no Mathlib proof is vendored.
The functor taking a covering space of X to the fibre over x₀, equipped with the
monodromy action of π₁(X, x₀).
It is assembled from the monodromy functor by restricting a fundamental-groupoid action along
the vertex-group inclusion TauCeti.Groupoid.singleObjFunctor and reading the result as an
action. It is @[expose]d so that its values hold by rfl in downstream modules.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The underlying set of the fundamental-group set attached to a cover is the fibre over the basepoint.
A loop class acts on the fibre over the basepoint by monodromy.
The MulAction carried by the fundamental-group set attached to a cover is Mathlib's
monodromy action on the fibre.
A map of covering spaces acts on the fibre over the basepoint by restriction.
Over a path-connected base, the fibre-action functor is faithful: the fundamental groupoid is
connected, so restricting its actions to the vertex group at x₀ is an equivalence.
Over a path-connected, locally path-connected base, the fibre-action functor is full: every
π₁(X, x₀)-equivariant map of fibres over x₀ is induced by a map of covering spaces.
The fibre-action functor is an equivalence: it is the composite of the monodromy equivalence, restriction along the connected groupoid's vertex-group inclusion, and Mathlib's identification of functors out of a one-object category with actions.
Covering spaces of X are equivalent to π₁(X, x₀)-sets.
Over a path-connected, locally path-connected, semilocally simply connected base, taking the
fibre over x₀ with its monodromy action is an equivalence of categories.
Equations
Instances For
The fundamental-group set attached to a connected covering space is transitive.
The fibre-action functor restricted to connected covering spaces and transitive fundamental-group sets.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The underlying fundamental-group set of a connected cover is the one attached to it as a cover.
The underlying map of fundamental-group sets assigned to a map of connected covers is the one
assigned to it as a map of covers, hence restriction to the fibres over x₀.
Every transitive π₁(X, x₀)-set is the fibre action of a connected cover. The cover is
the quotient of the universal cover by the stabiliser of a point of the set.
Connected covering spaces of X are equivalent to transitive π₁(X, x₀)-sets.