Let be a topological space which is well-connected in that it is
There is a functorial construction of a universal covering space of a pointed space
where is the full subcategory of with objects the well-connected spaces and is the subcategory of of pointed maps of spaces with objects the covering space maps.
Specifically, if is a space with basepoint , we define to be the space whose points are homotopy classes of paths in starting at , with the projection projecting to the endpoint of a path. We can equip this set with a topology coming from so that it becomes a universal covering space as above. As described at covering space, under the correspondence between covering spaces and -actions, the space corresponds to the “regular representation” of .
This regular representation can be seen to arise by taking a category of elements in the same way that the regular representation of a group is gotten by taking its action on itself: we can see that the universal covering groupoid in the slice category (see the universal covering -groupoid below) is just the category of elements of the action of on itself, and can be topologized in a natural way by lifting the topology on along the canonical projection ; decategorifying this yields .
We describe now how the universal cover construction may be understood from the nPOV. The basic idea is that the universal cover of a space is the (homotopy) fiber of the map from to its fundamental groupoid. We can think of this as a way of precisely saying “make trivial in a universal way.” There are at least two slightly different ways of making this precise in the language of -toposes, depending on whether we view as a little topos or as an object of a big topos.
that includes as the collection of constant paths.
Urs Schreiber: may need polishing.
Let be the set of connected components of , regarded as a topological -groupoid, and choose any section of the projection .
We think of this topological -groupoid as the universal covering -groupoid of . To break this down, we check that its decategorification gives the ordinary universal covering space:
for this we compute the homotopy pullback
where we assume to be connected with chosen baspoint just to shorten the exposition a little. By the laws of homotopy pullbacks in general and homotopy fibers in particular, we may compute this as the ordinary pullback of a weakly equivalent diagram, where the point is resolved to the universal -principal bundle
(More in detail, what we do behind the scenes is this: we regard the diagram as a diagram in the global model structure on simplicial presheaves on Top. In there all our topological groupoids are fibrant, hence all we have to ensure is that one of the morphisms of the diagram becomes a fibration, which is what the passage to achieves. Then the ordinary pullback in the category of simplicial presheaves is the homotopy pullback in -prestacks. Then by left exactness of -stackification, the image of that in -stacks is still a homotopy pullback. )
The topological groupoid has as objects homotopy classes rel endpoints of paths in starting at and as morphisms it has commuting triangles
in . The topology on this can be deduced from thinking of this as the pullback
in simplicial presheaves on Top. Unwinding what this means we find that the open sets in are those where the endpoint evaluation produces an open set in .
Now it is immediate to read off the homotopy pullback as the ordinary pullback
Since is categorically discrete, this simply produces the space of objects of over the points of , which is just the space of all paths in starting at with the projection being endpoint evaluation.
This indeed is then the usual construction of the universal covering space in terms of paths, as described for instance in
On the other hand, we can view a space as the little -topos of -sheaves on . If is locally connected and locally simply connected in the “coverings” sense, then is locally 1-connected.
In fact, for the construction of the universal cover we require only the (2,1)-topos of sheaves (stacks) of groupoids on , so we will work in that context because it is simpler. The construction can be adapted, however, to produce a “universal cover” of any locally 1-connected -topos.
Let be any (2,1)-topos which is locally 1-connected. This means that in the unique global sections geometric morphism , the functor has a left adjoint , which is automatically -indexed. The fundamental groupoid of is defined to be , where is the terminal object of .
As discussed here in the -case, the construction of is a left adjoint to the inclusion of groupoids into locally 1-connected (2,1)-toposes (which sends ). Thus we have a geometric morphism (where we regard as the (2,1)-topos ).
Suppose, for simplicity, that is connected. Then is also connected, and so we have an essentially unique functor . We define the universal cover of to be the pullback (2,1)-topos:
(where of course denotes the terminal (2,1)-topos ).
Now observe that is a local homeomorphism of toposes, since we have . Since local homeomorphisms of toposes are stable under pullback, is also a local homeomorphism, i.e. there exists an object and an equivalence over . Moreover, it is not hard to see that can be identified with the pullback
in . Note that the bottom map is applied to the unique map , while the right-hand map is the unit of the adjunction .
In order to see that this is a sensible definition, we first observe that is itself locally 1-connected (since it is etale over ). Moreover, it is actually 1-connected, which is equivalent to saying that . This is because the “Frobenius reciprocity” condition for the adjunction (which is equivalent to saying that is -indexed) applied to the defining pullback of implies that we also have a pullback
which clearly implies that .
Thus, is a connected and simply connected space with a local homeomorphism to , but is it a covering space? In other words, is it locally trivial? Since we have supposed that is locally 1-connected, as a (2,1)-category it can be generated by 1-connected objects, i.e. objects such that . In particular, we have a 1-connected object and a regular 1-epic? .
We claim that if is any 1-connected object of , then is trivialized (or split) over , in that is equivalent, over , to for some . For pulling back the defining pullback to , we obtain
But , so to give a map over is the same as to give a map in . But , since is 1-connected, and is connected, so there is only one such morphism. Therefore, the two maps in the pullback above are in fact the same, and in particular both are the pullback to of the map . Thus, is equivalent to , where is the loop object of , i.e. what we might call the fundamental group of the connected (2,1)-topos .
Therefore, since is trivialized over any 1-connected object, and is generated by 1-connected objects, is locally trivial. Moreover, since is a discrete object of , so is . Thus, if we specialize all this to the case of (2,1)-sheaves on a topological space, then we conclude that is an honest 1-sheaf on which, when regarded as a local homeomorphism over , is locally trivial (hence a covering space), connected, and 1-connected—i.e. a universal cover of .
The nPOV descriptions above lend themselves easily to generalization.
Urs Schreiber: here is something that I am thinking about.
Let be a locally ∞-connected (∞,1)-topos . Write
for the internal homotopy ∞-groupoid? functor.
For , the universal geometric -connected cover of is the homotopy fiber of .
We have that .
A homotopy-commuting diagram
in corresponds by the adjunction relation to diagram
in ∞Grpd. This being universal means that is -connected, and universal with that property as an object over .
By running this construction through the Postnikov tower for , we obtain the Whitehead tower in an (∞,1)-topos
If we instead generalize the “little topos” picture, then if is an -topos (or, more generally, an -topos) which is locally -connected, we have an -groupoid and we can define the universal -connected cover as the pullback topos
The same arguments as above, generalized from 1 to , show that is a locally trivial local homeomorphism and that is -connected.
See the references at covering space.