Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
  
  
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeMar 5th 2010
   • (edited Mar 5th 2010)
   • PermaLink
   Author: Urs
   Format: Markdownedited [[universal covering space]] * moved my proof to here that it is the homotopy fiber of the morphism <latex> X \to \Pi_1(X) </latex> of topological groupoids; * then created a new section <a href="http://ncatlab.org/nlab/show/universal+covering+space#InInftTopos">universal covering spaces in an (oo,1)-topos</a> where I talk about an idea (the evident idea) for what one should say here. * Also propose a definition for Whitehead tower in an (oo,1)-topos this way. * the entry [[Postnikov tower in an (infinity,1)-category]] following JL is under way...

   edited universal covering space

   • moved my proof to here that it is the homotopy fiber of the morphism of topological groupoids;

   • then created a new section universal covering spaces in an (oo,1)-topos where I talk about an idea (the evident idea) for what one should say here.

   • Also propose a definition for Whitehead tower in an (oo,1)-topos this way.

   • the entry Postnikov tower in an (infinity,1)-category following JL is under way...

2. • CommentRowNumber2.
   • CommentAuthorDavidRoberts
   • CommentTimeMar 5th 2010
   • PermaLink
   Author: DavidRoberts
   Format: TextThanks for that. I noticed I wrote something about doing this a long time ago.

   Thanks for that. I noticed I wrote something about doing this a long time ago.
3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeJul 2nd 2017
   • PermaLink
   Author: Urs
   Format: MarkdownItexI have added a little more point-set details to the bginning at _[[universal covering space]]_.

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

4. • CommentRowNumber4.
   • CommentAuthorTodd_Trimble
   • CommentTimeJul 3rd 2017
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexI 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$: $$\array{ & & \Delta \Gamma X & \leftarrow & \widetilde{X} & \stackrel{\gamma}{\to} & \Delta \Pi_0(\widetilde{X}) & & \\ & \mathllap{i} \swarrow & & (pb) & \downarrow & (po) & \downarrow & & \\ X & \stackrel{eval_1}{\leftarrow} & X^I & \leftarrow & P & \to & \widehat{X} & \stackrel{p}{\to} & X\\ & & \mathllap{eval_0} \downarrow & (pb) & \downarrow & \swarrow & & & \\ & & X & \underset{i}{\leftarrow} & \Delta \Gamma 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 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” -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 with its projection :

   I should explain the notation. We have a cohesive string of adjoints which is just what you expect: is the underlying set functor, and take sets to the associated discrete and codiscrete spaces, and 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 is a counit for , and the map is a unit for . The rest of the notation should be self-explanatory.

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

   here we construct a space , the coproduct over all such , as the pullback at the bottom left. The you see at top is similarly formed as a pullback; geometrically it’s the coproduct of spaces where is the space of paths from point to point . Thus would be the hom-set of the fundamental groupoid, and is the coproduct of all hom-sets of (seen as a discrete space). The right map along the top sends a path to its homotopy-rel-boundary class. Thus when we push out to get , we get homotopy-rel-boundary classes of elements of , which is exactly what we want for the unbiased universal covering space. (I’ll continue in the next comment.)

5. • CommentRowNumber5.
   • CommentAuthorTodd_Trimble
   • CommentTimeJul 3rd 2017
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexThe 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.

   The composite map factors through , and that’s where comes from. (Again, all of this follows I believe from purely formal properties of cohesion.) Of course

   is a monoid in the category of endospans (namely the fundamental groupoid), and the span

   carries a canonical module structure over this monoid (I guess a right module – whatever it is you call a functor ). If is a left module, then you can form a tensor product or weighted colimit , an object of , in fact when you form that span composition an object of and indeed a covering space over . Then

   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 -categories”, following these developments naturally as it were, is maybe best viewed in a cohesive context.

6. • CommentRowNumber6.
   • CommentAuthorDavidRoberts
   • CommentTimeJul 3rd 2017
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexYou'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).

   You’d want some sort of semi-local simple-connectedness to get local triviality of your , and for the higher stages of the Whitehead tower of , local -connectedness and semilocal -connectedness in order to get a locally constant stack of -groupoids of local sections.

   There is work by Jeremy Brazas on the setup when you lose the nice local homotopical conditions, so that 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).

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeJul 3rd 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexInteresting! Fills me with questions. 1. 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}$? 2. 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? 3. 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$?

   Interesting! Fills me with questions.

   1. 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 ?
   2. What do you get if you do it all homotopically, i.e. use ʃ instead of and a homotopy pushout instead of a set-pushout?
   3. What if instead of the pushout, we considered as living over (i.e. ) and take its fiberwise ʃ or ?
8. • CommentRowNumber8.
   • CommentAuthorDavidRoberts
   • CommentTimeJul 3rd 2017
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItex@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!

   @Mike Todd has explained this construction before, but not using formal cohesion. Essentially any two copies of a universal cover of a component corresponding to basepoints get identified as there is an arrow between them in . 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 , but this does away with that by using every single point, then gluing them all back together. It’s really very nice!

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeJul 3rd 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexBut 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?

   But the pushout all happens over the bottom copy of , so it seems to me that it can’t identify things in one component of with another?

10. • CommentRowNumber10.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexThat map $\widehat{X}\to \Delta\Gamma X$ looks wrong to me. Where does it come from?

    That map looks wrong to me. Where does it come from?

11. • CommentRowNumber11.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 3rd 2017
    • (edited Jul 3rd 2017)
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItex(duplicate)

    (duplicate)

12. • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeJul 3rd 2017
    • (edited Jul 3rd 2017)
    • PermaLink
    Author: Urs
    Format: MarkdownItexMike, the version in $\infty$-cohesion is what we have in the $n$Lab entry since [rev 6](https://ncatlab.org/nlab/revision/universal+covering+space/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.

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

    over any point (if is connected).

    (As one runs through the truncation degree 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 (the points-to-pieces transform). This would give the -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 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 .” 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 along something like the “smallest 1-epimorphism-when-evaluated-on-manifolds out of a 0-truncated object”, namely the morphism (from closed differental -forms to the coefficients for degree 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 -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.

13. • CommentRowNumber13.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItex>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!

    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!

14. • CommentRowNumber14.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexGuys, 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.

    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 , which is induced from the map . Set-theoretically it’s supposed to take an equivalence class of paths to . I think it’s well-defined because two paths map to the same in iff when we regard as belonging to (remember that set-theoretically is an identity because it’s a pullback of the set-theoretic identity map on the left), we have : that only happens if (call it ) and (call it ) and there’s a path between in (homotopy-rel-boundary). Anyway, we do have , so is well-defined.

15. • CommentRowNumber15.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexHmm, 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...

    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 . But perhaps that’s just experience with pointed covering spaces talking…

16. • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThanks 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.

    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.

17. • CommentRowNumber17.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItex@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)$!

    @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 !

18. • CommentRowNumber18.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexDavid: yes. And you raise a good point. I'd like to mull over that further...

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

19. • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeJul 3rd 2017
    • (edited Jul 3rd 2017)
    • PermaLink
    Author: Urs
    Format: MarkdownItexI 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](https://ncatlab.org/nlab/show/universal%20covering%20space#InCohesiveHomotopyTheory)_. 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!

    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 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 -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 -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!

20. • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeJul 3rd 2017
    • (edited Jul 3rd 2017)
    • PermaLink
    Author: Urs
    Format: MarkdownItexRegarding 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](https://ncatlab.org/nlab/show/Aufhebung#ExamplesBecomingFormalization)), with its minimal solution necessarily being Boolean ([this remark](https://ncatlab.org/nlab/show/Aufhebung#OnDoubleNegation)) 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.

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

    From the discussion of the sharp modality as the Aufhebung of the initial opposition (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.

21. • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI 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.

    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.

22. • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeJul 4th 2017
    • PermaLink
    Author: Urs
    Format: MarkdownItexDo you know if the internal real cohesion satisfies the property that shape preserves pullbacks over discrete types?

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

23. • CommentRowNumber23.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 9th 2021
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI see Peter Scholze returned to an MO question on universal covers from a condensed mathematics perspective [here](https://mathoverflow.net/a/383394/447). Presumably cohesive homotopy types can do a similar job.

    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.

24. • CommentRowNumber24.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 9th 2021
    • (edited Feb 9th 2021)
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexOh, maybe David R.'s new [answer](https://mathoverflow.net/a/383397/447) is about working in a cohesive setting. Felix and David Jaz Myers have approached this in cohesive type theory, [here](https://golem.ph.utexas.edu/category/2020/03/pyknoticity_versus_cohesivenes.html#c057759). Of course, the ingredients are already on this page.

    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.

25. • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeDec 25th 2021
    • PermaLink
    Author: Urs
    Format: MarkdownItexadded 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](https://link.springer.com/book/9780387902715)) 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]( https://doi.org/10.1515/9783110858372)) for generalization to equivariant homotopy theory. <a href="https://ncatlab.org/nlab/revision/diff/universal+covering+space/25">diff</a>, <a href="https://ncatlab.org/nlab/revision/universal+covering+space/25">v25</a>, <a href="https://ncatlab.org/nlab/show/universal+covering+space">current</a>

    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.

    diff, v25, current

26. • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeDec 26th 2021
    • (edited Dec 26th 2021)
    • PermaLink
    Author: Urs
    Format: MarkdownItexprodded by the exchange at "fundamental theorem of covering spaces" ([here](https://nforum.ncatlab.org/discussion/13742/fundamental-theorem-of-covering-spaces/?Focus=97059#Comment_97059)) have added pointer to definition of universal covering spaces in cohesive homotopy theory * [Def. 3.8.10](https://arxiv.org/pdf/1310.7930v1.pdf#page=356) in *[[schreiber:differential cohomology in a cohesive topos|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](https://arxiv.org/abs/2003.09713), [doi:10.1017/S0960129520000201](https://doi.org/10.1017/S0960129520000201)) <a href="https://ncatlab.org/nlab/revision/diff/universal+covering+space/26">diff</a>, <a href="https://ncatlab.org/nlab/revision/universal+covering+space/26">v26</a>, <a href="https://ncatlab.org/nlab/show/universal+covering+space">current</a>

    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)

    diff, v26, current

27. • CommentRowNumber27.
    • CommentAuthorDmitri Pavlov
    • CommentTimeNov 17th 2023
    • PermaLink
    Author: Dmitri Pavlov
    Format: MarkdownItexAdded: A detailed treatment is available in * [[Nicolas Bourbaki]], _Topologie Algébrique_, Chapitres 1 à 4, Springer, 2016. [doi:10.1007/978-3-662-49361-8](https://doi.org/10.1007/978-3-662-49361-8), ISBN 978-3-662-49361-8. <a href="https://ncatlab.org/nlab/revision/diff/universal+covering+space/29">diff</a>, <a href="https://ncatlab.org/nlab/revision/universal+covering+space/29">v29</a>, <a href="https://ncatlab.org/nlab/show/universal+covering+space">current</a>

    Added:

    A detailed treatment is available in

    • Nicolas Bourbaki, Topologie Algébrique, Chapitres 1 à 4, Springer, 2016. doi:10.1007/978-3-662-49361-8, ISBN 978-3-662-49361-8.

    diff, v29, current