Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

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 comma complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite 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 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

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeMar 5th 2010
    • (edited Mar 5th 2010)

    edited universal covering space

    • CommentRowNumber2.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 5th 2010
    Thanks for that. I noticed I wrote something about doing this a long time ago.
    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeJul 2nd 2017

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

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 3rd 2017

    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” nn-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 X^\widehat{X} with its projection p:X^Xp: \widehat{X} \to X:

    ΔΓX X˜ γ ΔΠ 0(X˜) i (pb) (po) X eval 1 X I P X^ p X eval 0 (pb) X i ΔΓ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 Π 0ΔΓ:SetLocConn\Pi_0 \dashv \Delta \dashv \Gamma \dashv \nabla: Set \to LocConn which is just what you expect: Γ=hom(1,)\Gamma = \hom(1,-) is the underlying set functor, Δ\Delta and \nabla take sets to the associated discrete and codiscrete spaces, and Π 0\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:ΔΓXXi: \Delta \Gamma X \to X is a counit for ΔΓ\Delta \dashv \Gamma, and the map γ:X˜ΔΠ 0X˜\gamma: \widetilde{X} \to \Delta \Pi_0 \widetilde{X} is a unit for Π 0Δ\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 xx of the base space and looks at homotopy-rel-boundary classes of paths in XX whose starting point of xx. The construction above does something similar except that it considers all possible basepoints (hence, “unbiased”). So, whereas in the ordinary construction one chooses an xXx \in X and constructs the space of paths P xP_x emanating from xx as a pullback

    P x X I eval 0 1 x X\array{ P_x & \to & X^I \\ \downarrow & & \downarrow \mathrlap{eval_0} \\ 1 & \underset{x}{\to} & X }

    here we construct a space P= xXP xP = \sum_{x \in X} P_x, the coproduct over all such P xP_x, as the pullback at the bottom left. The X˜\widetilde{X} you see at top is similarly formed as a pullback; geometrically it’s the coproduct of spaces (x,y)X×XX˜(x,y)\sum_{(x, y) \in X \times X} \widetilde{X}(x, y) where X˜(x,y)\widetilde{X}(x, y) is the space of paths from point xx to point yy. Thus Π 0(X˜(x,y))\Pi_0(\widetilde{X}(x, y)) would be the hom-set Π 1(X)(x,y)\Pi_1(X)(x, y) of the fundamental groupoid, and ΔΠ 0(X˜)\Delta \Pi_0(\widetilde{X}) is the coproduct of all hom-sets of Π 1(X)\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 PX^P \to \widehat{X}, we get homotopy-rel-boundary classes of elements of PP, which is exactly what we want for the unbiased universal covering space. (I’ll continue in the next comment.)

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 3rd 2017

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

    ΔΠ 0X˜=Π 1(X) ΔΓX ΔΓX\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

    X^ p ΔΓX X\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 Π 1(X) opTop\Pi_1(X)^{op} \to Top). If F:Π 1(X)SetF: \Pi_1(X) \to Set is a left module, then you can form a tensor product or weighted colimit X^ Π 1(X)F\widehat{X} \otimes_{\Pi_1(X)} F, an object of TopTop, in fact when you form that span composition an object of Top/XTop/X and indeed a covering space over XX. Then

    X^ Π 1(X):Set Π 1(X)Cov/X\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 nn-categories”, following these developments naturally as it were, is maybe best viewed in a cohesive context.

    • CommentRowNumber6.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 3rd 2017

    You’d want some sort of semi-local simple-connectedness to get local triviality of your X˜X\widetilde{X}\to X, and for the higher stages of the Whitehead tower of XX, local (n1)(n-1)-connectedness and semilocal nn-connectedness in order to get a locally constant stack of (n1)(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 π 1\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).

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeJul 3rd 2017

    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 X^\widehat{X}?
    2. What do you get if you do it all homotopically, i.e. use ʃ instead of Π 0\Pi_0 and a homotopy pushout instead of a set-pushout?
    3. What if instead of the pushout, we considered PP as living over X×XX\times \flat X (i.e. X×ΔΓXX\times \Delta\Gamma X) and take its fiberwise ʃ or Π 0\Pi_0?
    • CommentRowNumber8.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 3rd 2017

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

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeJul 3rd 2017

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

    • CommentRowNumber10.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 3rd 2017

    That map X^ΔΓX\widehat{X}\to \Delta\Gamma X looks wrong to me. Where does it come from?

    • CommentRowNumber11.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 3rd 2017
    • (edited Jul 3rd 2017)

    (duplicate)

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeJul 3rd 2017
    • (edited Jul 3rd 2017)

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

    XΔΠ 1(X)=τ 1ʃX X \longrightarrow \Delta \Pi_1(X) = \tau_1 ʃ X

    over any point (if XX is connected).

    (As one runs through the truncation degree τ n\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 X=ΔΓΔΠ 1X\flat X = \Delta \Gamma \to \Delta \Pi_1 X (the points-to-pieces transform). This would give the ΓX\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 π 0(X)=τ 0(ΔΠ 1X)ΔΠ 1X\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 ΔΠ 1X\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 B nB n\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 Ω cl nB n\Omega^n_{cl} \longrightarrow \mathbf{B}^n \mathbb{R} (from closed differental nn-forms to the coefficients for degree nn 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.

    • CommentRowNumber13.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 3rd 2017

    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!

    • CommentRowNumber14.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 3rd 2017

    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 ΔΓXX^\Delta \Gamma X \leftarrow \widehat{X}, which is induced from the map PΔΓXP \to \Delta \Gamma X. Set-theoretically it’s supposed to take an equivalence class of paths [α][\alpha] to α(0)\alpha(0). I think it’s well-defined because two paths α,βP\alpha, \beta \in P map to the same [α]=[β][\alpha] = [\beta] in X^\widehat{X} iff when we regard α,β\alpha, \beta as belonging to X˜\widetilde{X} (remember that set-theoretically X˜P\widetilde{X} \to P is an identity because it’s a pullback of the set-theoretic identity map ΔΓXX\Delta \Gamma X \to X on the left), we have γ(α)=γ(β)\gamma(\alpha) = \gamma(\beta): that only happens if α(0)=β(0)\alpha(0) = \beta(0) (call it xx) and α(1)=β(1)\alpha(1) = \beta(1) (call it yy) and there’s a path between α,β\alpha, \beta in X˜(x,y)\widetilde{X}(x, y) (homotopy-rel-boundary). Anyway, we do have α(0)=β(0)\alpha(0) = \beta(0), so [α]α(0)[\alpha] \mapsto \alpha(0) is well-defined.

    • CommentRowNumber15.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 3rd 2017

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

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeJul 3rd 2017

    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.

    • CommentRowNumber17.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 3rd 2017

    @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ΔΠ 0(X)X\to \Delta\Pi_0(X)!

    • CommentRowNumber18.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 3rd 2017

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

    • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeJul 3rd 2017
    • (edited Jul 3rd 2017)

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

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeJul 3rd 2017
    • (edited Jul 3rd 2017)

    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.

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeJul 3rd 2017

    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.

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeJul 4th 2017

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

    • CommentRowNumber23.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 9th 2021

    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.

    • CommentRowNumber24.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 9th 2021
    • (edited Feb 9th 2021)

    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.

    • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeDec 25th 2021

    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

    for generalization to equivariant homotopy theory.

    diff, v25, current

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeDec 26th 2021
    • (edited Dec 26th 2021)

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

    have added pointer to definition of universal covering spaces

    in cohesive homotopy theory

    and explicitly so in cohesive homotopy type theory:

    diff, v26, current

    • CommentRowNumber27.
    • CommentAuthorDmitri Pavlov
    • CommentTimeNov 17th 2023

    Added:

    A detailed treatment is available in

    diff, v29, current