prodded by the exchange at “fundamental theorem of covering spaces” (here)

have added pointer to definition of universal covering spaces

in cohesive homotopy theory

- Def. 3.8.10 in
*dcct*

and explicitly so in cohesive homotopy type theory:

- Felix Cherubini, Egbert Rijke, Def. 8.5:
*Modal Descent*, Mathematical Structures in Computer Science (2020) (arXiv:2003.09713, doi:10.1017/S0960129520000201)

added pointer to

- William S. Massey, Chapter 5, Section 10 of:
*Algebraic Topology: An Introduction*, Harcourt Brace & World 1967, reprinted in: Graduate Texts in Mathematics, Springer 1977 (ISBN:978-0-387-90271-5)

for an original reference (maybe the construction via equivalence classes of based paths originates with the discussion on p. 175 here?)

and pointer to

- Tammo tom Dieck, Section I (10.13) of:
*Transformation Groups*, de Gruyter 1987 (doi:10.1515/9783110858372)

for generalization to equivariant homotopy theory.

]]>Oh, maybe David R.’s new answer is about working in a cohesive setting.

Felix and David Jaz Myers have approached this in cohesive type theory, here.

Of course, the ingredients are already on this page.

]]>I see Peter Scholze returned to an MO question on universal covers from a condensed mathematics perspective here. Presumably cohesive homotopy types can do a similar job.

]]>Do you know if the internal real cohesion satisfies the property that shape preserves pullbacks over discrete types?

]]>I would be somewhat doubtful that local contractibility is enough, but I could be wrong. My hope would instead be that the identification can be proved *internally* from the real-cohesion axiom.

Regarding choice: Right, I am tacitly assuming choice in the base topos.

From the discussion of the sharp modality $\sharp$ as the Aufhebung of the initial opposition $\emptyset \dashv \ast$ (here), with its minimal solution necessarily being Boolean (this remark) I grew fond of the idea that it is quite natural to assume the base of a cohesive theory to be classical. I might go as far as feeling that this neatly captures the whole dichotomy between classical and constructive logics: we do want both, but the former precisely only in the base of discrete types, while the latter in the full theory of cohesive types.

In any case, if we don’t allow ourselves to choose single basepoints at all, then I don’t see how to get rid of the the spurious copies of the universal covering space.

]]>I have written out now the *abstract* argument that the definition in cohesive homotopy theory comes out right, this is now the first part of the section (now) titled *Universal covering space – In cohesive homotopy theory*.

The previous argument that used to be in the entry (now the second part of that section, not notationally harmonized yet), argues that the homotopy fiber of the morphism from $X$ to its fundamental groupoid, both regarded as topological stacks, canonically yields the classical construction via homotopy classes of paths, the way Todd is discussing above. For this to be a special case of this abstract construction one needs a result, namely that the shape modality is represented by a “path $\infty$-groupoid”.

This is true in “Euclidean topological infinity-groupoids” at least, due to a result that Dmiti Pavlov has announced long ago, following a similar result by Bunke-Nikolaus-Völkl. I am recording this now at *shape via cohesive path ∞-groupoid*.

One would like this to be true also over the $\infty$-cohesive site of locally contractible topological spaces (or at least over the 1-cohesive site of locally simply connected topological spaces), but I don’t know if it is. Somebody should think about this!

]]>David: yes. And you raise a good point. I’d like to mull over that further…

]]>@Mike

assuming the axiom of choice in the discrete world (right?)

of course, and that’s a reason to use the cohesive treatment over the version that assumes one has a section of $X\to \Delta\Pi_0(X)$!

]]>Thanks Urs! Do you think that can be made to coincide formally with Todd’s definition?

This is not as bad as it sounds, since this section is essentially unique.

its mere existence is unique

… assuming the axiom of choice in the discrete world (right?). (-: Otherwise it might not exist at all. In fact, if sets cover fails, there may not be any epimorphism to an object out of a 0-truncated one.

]]>Hmm, so you *do* have a disjoint union of simply-connected covering spaces, one for each point of the space? To my mind, a universal covering space of a disconnected space should induce an isomorphism on $\Pi_0$. But perhaps that’s just experience with pointed covering spaces talking…

Guys, thanks very much for your interest and questions! I’m going to be very busy today with other things, but I’m looking forward to getting back to this soon, hopefully by sometime tomorrow. I can tell I’m going to learn a great deal from this, and I’m sure to have questions in return.

I did want to address David’s question in #10 about $\Delta \Gamma X \leftarrow \widehat{X}$, which is induced from the map $P \to \Delta \Gamma X$. Set-theoretically it’s supposed to take an equivalence class of paths $[\alpha]$ to $\alpha(0)$. I think it’s well-defined because two paths $\alpha, \beta \in P$ map to the same $[\alpha] = [\beta]$ in $\widehat{X}$ iff when we regard $\alpha, \beta$ as belonging to $\widetilde{X}$ (remember that set-theoretically $\widetilde{X} \to P$ is an identity because it’s a pullback of the set-theoretic identity map $\Delta \Gamma X \to X$ on the left), we have $\gamma(\alpha) = \gamma(\beta)$: that only happens if $\alpha(0) = \beta(0)$ (call it $x$) and $\alpha(1) = \beta(1)$ (call it $y$) and there’s a path between $\alpha, \beta$ in $\widetilde{X}(x, y)$ (homotopy-rel-boundary). Anyway, we do have $\alpha(0) = \beta(0)$, so $[\alpha] \mapsto \alpha(0)$ is well-defined.

]]>This is not as bad as it sounds, since this section is essentially unique.

its mere existence is unique, but it can have many automorphisms!

]]>Mike, the version in $\infty$-cohesion is what we have in the $n$Lab entry since rev 6 in 2010: the universal covering space is the homotopy fiber of

$X \longrightarrow \Delta \Pi_1(X) = \tau_1 ʃ X$over any point (if $X$ is connected).

(As one runs through the truncation degree $\tau_n$ here, one obtains the whole Whitehead tower. This is something that David Roberts and myself made notes about years ago at *Whitehead tower in an (infinity,1)-topos*. Looking back at it, it could do with some polishing.)

If we don’t like to choose a point, we could instead take the homotopy fiber product with $\flat X = \Delta \Gamma \to \Delta \Pi_1 X$ (the points-to-pieces transform). This would give the $\Gamma X$-many-copies-version of the covering space which Todd is considering above.

In the entry instead the perspective is taken that one takes the fiber product along a choice of section $\pi_0(X) = \tau_0(\Delta \Pi_1 X) \to \Delta \Pi_1 X$ of the 0-truncation. This is not as bad as it sounds, since this section is essentially unique.

But I am inclined to view this as the pullback along something like the “smallest 1-epimorphism out of a 0-truncated object into $\Delta \Pi_1 X$.” I wish I had a solid general definition of what this should be, because something similar happens in the definition of ordinary differential cohomology:

There we form the homotopy fiber product of a canonical map $\mathbf{B}^n \mathbb{Z} \to \mathbf{B}^n \mathbb{Z}$ along something like the “smallest 1-epimorphism-when-evaluated-on-manifolds out of a 0-truncated object”, namely the morphism $\Omega^n_{cl} \longrightarrow \mathbf{B}^n \mathbb{R}$ (from closed differental $n$-forms to the coefficients for degree $n$ real cohomology, which is an epimorphism when evaluated on manifolds (or anything smooth with a partition of unity) by the de Rham theorem).

So it seems a common theme that we want to take homotopy fibers of morphisms into some $\infty$-stack by choosing a smallest 0-truncated object that hits all the connected components of the thing we are pullback back over, at least after evaluating everything on some prescribed class of objects. I keep wanting to have a good general formalization of this rough idea. It might be the answer to some other open problems that I have.

]]>(duplicate)

]]>That map $\widehat{X}\to \Delta\Gamma X$ looks wrong to me. Where does it come from?

]]>But the pushout all happens over the bottom copy of $\Delta\Gamma X$, so it seems to me that it can’t identify things in one component of $P$ with another?

]]>@Mike Todd has explained this construction before, but not using formal cohesion. Essentially any two copies of a universal cover of a component $X_\alpha \subset X$ corresponding to basepoints $x_1,s_2$ get identified as there is an arrow between them in $\Pi_1(X)$. A homotopy pushout would remember *which* arrow one is using to identify these two covering spaces.

Note that Ronnie Brown would be happy to only go halfway and choose a basepoint in each path component of $X$, but this does away with that by using every single point, then gluing them all back together. It’s really very nice!

]]>Interesting! Fills me with questions.

- Can you then extract a space that’s equivalent to the usual universal covering spaces, instead of a coproduct of a bunch of copies of it, by taking some kind of quotient of $\widehat{X}$?
- What do you get if you do it all homotopically, i.e. use ʃ instead of $\Pi_0$ and a homotopy pushout instead of a set-pushout?
- What if instead of the pushout, we considered $P$ as living over $X\times \flat X$ (i.e. $X\times \Delta\Gamma X$) and take its
*fiberwise*ʃ or $\Pi_0$?

You’d want some sort of semi-local simple-connectedness to get local triviality of your $\widetilde{X}\to X$, and for the higher stages of the Whitehead tower of $X$, local $(n-1)$-connectedness and semilocal $n$-connectedness in order to get a locally constant stack of $(n-1)$-groupoids of local sections.

There is work by Jeremy Brazas on the setup when you lose the nice local homotopical conditions, so that $\pi_1$ is naturally a semitopological group (multiplication is separately continuous in each variable) as a quotient of the based loop space, and you can also put a group topology on it, and get the nice construction of universal “covering spaces” for that framework (fibres are no longer discrete, but one has good lifting properties).

]]>The composite map $X \stackrel{eval_1}{\leftarrow} X^I \leftarrow P$ factors through $P \to \widehat{X}$, and that’s where $p: \widehat{X} \to X$ comes from. (Again, all of this follows I believe from purely formal properties of cohesion.) Of course

$\array{ & & \Delta \Pi_0 \widetilde{X} = \Pi_1(X) & & \\ & \swarrow & & \searrow & \\ \Delta \Gamma X & & & & \Delta \Gamma X }$is a monoid in the category of endospans (namely the fundamental groupoid), and the span

$\array{ & & \widehat{X} & & \\ & \swarrow & & \searrow^\mathllap{p} & \\ \Delta \Gamma X & & & & X }$carries a canonical module structure over this monoid (I guess a right module – whatever it is you call a functor $\Pi_1(X)^{op} \to Top$). If $F: \Pi_1(X) \to Set$ is a left module, then you can form a tensor product or weighted colimit $\widehat{X} \otimes_{\Pi_1(X)} F$, an object of $Top$, in fact when you form that span composition an object of $Top/X$ and indeed a covering space over $X$. Then

$\widehat{X} \otimes_{\Pi_1(X)} -: Set^{\Pi_1(X)} \to Cov/X$is the left adjoint in the adjoint equivalence which expresses the fundamental theorem of covering space theory, but expressed in unbiased form.

I’m not sure where to find this in the literature (some authors come close but then pull back, somehow), but the thing I find pleasant is just how formal this is, and how much you can milk on the basis of so little (cohesion plus the topological interval as data). And it hadn’t occurred to me before that the machinery of “Trimble $n$-categories”, following these developments naturally as it were, is maybe best viewed in a cohesive context.

]]>I don’t mean to interrupt Urs’s train of thought (and he should feel free to ignore this while he’s hammering out details), but now returning to this topic about 7 years later, the general abstract construction of universal covering spaces in the context of cohesion seems sort of interesting to me. Part of this is the desire to get free from basepoints, and free from the path-connected assumption on the base space, and free from just groups, passing to groupoids, etc., and connect up with (so-called) “Trimble” $n$-categories…

Here is a diagram I’ve written down on my private web, an abstract construction of what I am provisionally calling the *unbiased* universal covering space $\widehat{X}$ with its projection $p: \widehat{X} \to X$:

I should explain the notation. We have a cohesive string of adjoints $\Pi_0 \dashv \Delta \dashv \Gamma \dashv \nabla: Set \to LocConn$ which is just what you expect: $\Gamma = \hom(1,-)$ is the underlying set functor, $\Delta$ and $\nabla$ take sets to the associated discrete and codiscrete spaces, and $\Pi_0$ is the (path-)connected components functor. (There are some point-set topology details I’m sliding over for the moment, so that we can consider the big picture.) The map $i: \Delta \Gamma X \to X$ is a counit for $\Delta \dashv \Gamma$, and the map $\gamma: \widetilde{X} \to \Delta \Pi_0 \widetilde{X}$ is a unit for $\Pi_0 \dashv \Delta$. The rest of the notation should be self-explanatory.

Ordinarily, when one constructs a universal covering space, one chooses a basepoint $x$ of the base space and looks at homotopy-rel-boundary classes of paths in $X$ whose starting point of $x$. The construction above does something similar except that it considers all possible basepoints (hence, “unbiased”). So, whereas in the ordinary construction one chooses an $x \in X$ and constructs the space of paths $P_x$ emanating from $x$ as a pullback

$\array{ P_x & \to & X^I \\ \downarrow & & \downarrow \mathrlap{eval_0} \\ 1 & \underset{x}{\to} & X }$here we construct a space $P = \sum_{x \in X} P_x$, the coproduct over all such $P_x$, as the pullback at the bottom left. The $\widetilde{X}$ you see at top is similarly formed as a pullback; geometrically it’s the coproduct of spaces $\sum_{(x, y) \in X \times X} \widetilde{X}(x, y)$ where $\widetilde{X}(x, y)$ is the space of paths from point $x$ to point $y$. Thus $\Pi_0(\widetilde{X}(x, y))$ would be the hom-set $\Pi_1(X)(x, y)$ of the fundamental groupoid, and $\Delta \Pi_0(\widetilde{X})$ is the coproduct of all hom-sets of $\Pi_1(X)$ (seen as a discrete space). The right map $\gamma$ along the top sends a path $\alpha$ to its homotopy-rel-boundary class. Thus when we push out $\gamma$ to get $P \to \widehat{X}$, we get homotopy-rel-boundary classes of elements of $P$, which is exactly what we want for the unbiased universal covering space. (I’ll continue in the next comment.)

]]>I have added a little more point-set details to the bginning at *universal covering space*.