nLab fundamental theorem of covering spaces




topology (point-set topology, point-free topology)

see also differential topology, algebraic topology, functional analysis and topological homotopy theory


Basic concepts

Universal constructions

Extra stuff, structure, properties


Basic statements


Analysis Theorems

topological homotopy theory

Homotopy theory

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed

models: topological, simplicial, localic, …

see also algebraic topology



Paths and cylinders

Homotopy groups

Basic facts






In topological homotopy theory, the fundamental theorem of covering spaces says that for a sufficiently well-behaved topological space XX, the functor which sends a covering space of XX to its monodromy Set-action (permutation representation) of the fundamental groupoid of XX on the fibers of EE is an equivalence of categories.

This is a basic instance of the general principle of Galois theory.

It follows in particular that for connected XX the automorphism group of the universal covering space of XX coincides with the fundamental group π 1(X,x)\pi_1(X,x) itself (for any basepoint xx). This often yields a convenient means to determine the fundamental group of XX in the first place.

This is closely related to the (∞,1)-Grothendieck construction; the equivalence Grpd /ʃXGrpd ʃX\infty Grpd_{/\esh X} \simeq \infty Grpd^{\esh X} restricts to an equivalence between the subcategories of bundles YʃXY \to \esh X with 0-truncated fibers and of set-valued functors on ʃX\esh X. Observe in particular that Set Π 1(X)Set ʃXSet^{\Pi_1(X)} \simeq Set^{\esh X}.

(Here ʃX\esh X denotes the shape of the topological space XX, hence its fundamental \infty -groupoid).



(fundamental theorem of covering spaces)

Let XX be a locally path-connected and semi-locally simply-connected topological space. Then the operations on

  1. extracting the monodromy Fib EFib_{E} of a covering space EE over XX

  2. reconstructing a covering space from monodromyRec(ρ)\; Rec(\rho)

constitute an equivalence of categories

Cov(X)FibRecSet Π 1(X) Cov(X) \underoverset {\underset{Fib}{\longrightarrow}} {\overset{Rec}{\longleftarrow}} {\simeq} Set^{\Pi_1(X)}

between the category of covering spaces, and the category of permutation groupoid representations of the fundamental groupoid of XX.


With the standard definitions of the two functors, both are in fact inverse isomorphisms of categories instead of just equivalences of categories (meaning that the required natural isomorphisms from the composites of the two functors to the identity functor are componentwise equalities), which establishes the claim right away. For definiteness, we make this explicit:

Given ρSet Π 1(X)\rho \in Set^{\Pi_1(X)} a permutation representation, we need to exhibit a natural isomorphism of permutation representations.

η ρ:ρFib(Rec(ρ)) \eta_{\rho} \;\colon\; \rho \longrightarrow Fib(Rec(\rho))

First consider what the right hand side is like: By this def. of RecRec and this def. of FibFib we have for every xXx \in X an actual equality

Fib(Rec(ρ))(x)=ρ(x). Fib(Rec(\rho))(x) = \rho(x) \,.

To similarly understand the value of Fib(Rec(ρ))Fib(Rec(\rho)) on morphisms [γ]Π 1(X)[\gamma] \in \Pi_1(X), let γ:[0,1]X\gamma \colon [0,1] \to X be a representing path in XX. As in the proof of the path lifting lemma for covering spaces (this lemma) we find a finite number of paths {γ i} i{1,n}\{\gamma_i\}_{i \in \{1,n\}} such that

  1. regarded as morphisms [γ i][\gamma_i] in Π 1(X)\Pi_1(X) they compose to [γ][\gamma]:

    [γ]=[γ n][γ 2][γ 1] [\gamma] = [\gamma_n] \circ \cdots \circ [\gamma_2] \circ [\gamma_1]
  2. each γ i\gamma_i factors through an open subset U iXU_i \subset X over which Rec(ρ)Rec(\rho) trivializes.

Hence by functoriality of Fib(Rec(ρ))Fib(Rec(\rho)) it is sufficient to understand its value on these paths γ i\gamma_i. But on these we have again by direct unwinding of the definitions that

Fib(Rec(ρ))([γ i])=ρ([γ i]). Fib(Rec(\rho))([\gamma_i]) = \rho([\gamma_i]) \,.

This means that if we take

η ρ(x):ρ(x)=Fib(Rec(ρ)) \eta_\rho(x) \colon \rho(x) \overset{=}{\longrightarrow} Fib(Rec(\rho))

to be the above identification, then this is a natural transformation and hence in a particular a natural isomorphism, as required.

It remains to see that these morphisms η ρ\eta_\rho are themselves natural in ρ\rho, hence that for each morphism ϕ:ρρ\phi \colon \rho \to \rho' the diagram

ρ ϕ ρ eta ρ η ρ Fib(Rec(ρ)) Fib(Rec(ϕ)) Fib(Rec(ρ)) \array{ \rho &\overset{\phi}{\longrightarrow}& \rho' \\ {}^{\mathllap{eta_\rho}}\downarrow && \downarrow^{\mathrlap{\eta_{\rho'}}} \\ Fib(Rec(\rho)) &\underset{Fib(Rec(\phi))}{\longrightarrow}& Fib(Rec(\rho')) }

commutes as a diagram in Rep(Π 1(X),Set)Rep(\Pi_1(X), Set). Since these morphisms are themselves groupoid homotopies (natural isomorphisms) this is the case precisely if for all xXx \in X the corresponding component diagram commutes. But by the above this is

ρ(x) ϕ(x) ρ(x) = = Fib(Rec(ρ))(x) Fib(Rec(ϕ))(x) Fib(Rec(ρ))(x) \array{ \rho(x) &\overset{\phi(x)}{\longrightarrow}& \rho'(x) \\ {}^{\mathllap{=}}\downarrow && \downarrow^{\mathrlap{=}} \\ Fib(Rec(\rho))(x) &\underset{Fib(Rec(\phi))(x) }{\longrightarrow}& Fib(Rec(\rho'))(x) }

and hence this means that the top and bottom horizontal morphism are in fact equal. Direct unwinding of the definitions shows that this is indeed the case.

Conversely, given ECov(X)E \in Cov(X) a covering space, we need to exhibit a natural isomorphism of covering spaces of the form

ϵ E:Rec(Fib(E))E. \epsilon_E \;\colon\; Rec(Fib(E)) \longrightarrow E \,.

Again by this def. of RecRec and this def. of FibFib the underlying set of Rec(Fib(E))Rec(Fib(E)) is actually equal to that of EE, hence it is sufficient to check that this identity function on underlying sets is a homeomorphism of topological spaces.

By the assumption that XX is locally path-connected and semi-locally simply connected, it is sufficient to check for UXU\subset X an open path-connected subset and xXx \in X a point with the property that π 1(U,x)π 1(X,x)\pi_1(U,x) \to \pi_1(X,x) lands is constant on the trivial element, that the open subsets of EE of the form U×{x^}p 1(U)U \times \{\hat x\} \subset p^{-1}(U) form a basis for the topology of Rec(Fib(E))Rec(Fib(E)). But this is the case by definition of RecRec.

It remains to see that ϵ E\epsilon_E is itself natural in EE. But as for the converse direction, since the components of ϵ E\epsilon_E are in fact equalities, this follows by direct unwinding of the definitions.

This establishes an equivalence as required. In fact this is an adjoint equivalence.


In homotopy type theory

In homotopy type theory, the fundamental theorem of covering spaces is really just a special case of the universal property of 1 1 -truncation.

Indeed, in HoTT a covering space over a type XX is usually defined as a dependent type C:XSetsC \colon X \to \mathsf{Sets}. We can get the more familiar bundle definition of a covering space by taking the dependent sum type x:XC(x)\sum_{x \colon X} C(x), which comes equipped with a canonical projection proj 1: x:XC(x)X\operatorname{proj}_1 \colon \sum_{x \colon X} C(x) \to X.

Since Sets\mathsf{Sets} is a 11-type, then by the universal property of 1-truncation we have an equivalence:

(X 1Sets)(XSets). \big( \Vert X \Vert_1 \to \mathsf{Sets} \big) \;\simeq\; \big( X \to \mathsf{Sets} \big) \,.

Since the 1-truncation X 1\Vert X \Vert_1 is the fundamental groupoid of XX, this really is the fundamental theorem of covering spaces.

Or rather, more faithful to the traditional concepts in topology, it is the shape modality ʃ\esh in cohesive homotopy type theory which turns a geometric homotopy type into XX its fundamental \infty -groupoid ʃX\esh X (see at shape via cohesive path ∞-groupoid) truncating to the actual fundamental groupoid ʃX 1\Vert \esh X \Vert_1.

Then the adjunction between the shape modality and the flat modality \flat says that

(ʃXSets)(XSets), \big( \esh X \to \mathsf{Sets} \big) \;\simeq\; \big( X \to \flat \mathsf{Sets} \big) \,,

or, equivalently, that

(ʃX 1Sets)(XSets), \big( \Vert \esh X \Vert_1 \to \mathsf{Sets} \big) \;\simeq\; \big( X \to \flat \mathsf{Sets} \big) \,,

where Sets\flat Sets is the actual classifier for covering spaces in the generality of cohesive (e.g. topological) homotopy types. This reflects the fundamental theorem of covering spaces as traditionally understood in topology.

This is the topic of dcct, sec. 3.8.6, p. 358, see also Cherubini & Rijke 2020, Thm. 8.7.


On the classical theory:

A detailed treatment is available in

Textbook account:

Lecture notes:

Discussion in cohesive homotopy theory:

Discussion in cohesive homotopy type theory:

Last revised on November 18, 2023 at 05:21:48. See the history of this page for a list of all contributions to it.