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 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 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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure 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).

nLab > Latest Changes: free loop space of classifying space

Bottom of Page

1 to 24 of 24

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeJul 3rd 2021

    am recording an actual proof that

    ℒ(W¯𝒢)≃𝒢 ad⫽𝒢 \mathcal{L} \big( \overline{W}\mathcal{G} \big) \;\; \simeq \;\; \mathcal{G}_{ad} \sslash \mathcal{G}

    I expected that a proof for this folklore theorem would be citeable from the literature, but maybe not quite. This MO reply points to Lemma 9.1 in arXiv:0811.0771, which has the idea (in topological spaces), but doesn’t explicitly verify all ingredients. I have tried to make it fully explicit (in simplicial sets).

    v1, current

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeJul 3rd 2021

    On the other hand, I haven’t yet managed to see a copy of

    which apparently has a discussion of the issue in its appendix.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeJul 4th 2021

    added pointer to the relevant 3 pages in

    • Kate Gruher, A proof of LBG≃Ad(EG)L B G \simeq Ad(E G), Appendix A in String Topology of Classifying Spaces, 2007 (pdf)

    diff, v3, current

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeJul 4th 2021

    Added some words (here) on the basic example of discrete groups, and then expanded the Idea-section a fair bit.

    diff, v4, current

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeJul 4th 2021

    added pointer to

    diff, v7, current

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeJul 9th 2021
    • (edited Jul 9th 2021)

    I have added an Examples-section (here) on the case that 𝒢=𝒜\mathcal{G} = \mathcal{A} is a simplicial abelian group,

    with statement and (immediate) proof of

    [Bℤ,B𝒜]≃𝒜×B𝒜. \big[ \mathbf{B}\mathbb{Z}, \, \mathbf{B}\mathcal{A} \big] \;\; \simeq \;\; \mathcal{A} \times \mathbf{B}\mathcal{A} \,.

    and with the example

    ℒB n+1A≃B nA×B n+1A, \mathcal{L} \mathbf{B}^{n+1}A \;\simeq\; \mathbf{B}^n A \,\times\, \mathbf{B}^{n+1}A \,,

    diff, v12, current

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJul 10th 2021

    Does anyone know or see how to make the simplicial presentation in the entry here functorial in W¯𝒢\overline{W}\mathcal{G}?

    I.e. for W¯𝒢⟶W¯𝒦\overline{W}\mathcal{G} \longrightarrow \overline{W}\mathcal{K} a morphism, do we have an induced morphism (W𝒢×𝒢 ad)/𝒢⟶(W𝒦×𝒦 ad)/𝒦\big( W\mathcal{G} \times \mathcal{G}_{ad}\big)/\mathcal{G} \longrightarrow \big( W\mathcal{K} \times \mathcal{K}_{ad}\big)/\mathcal{K} or does it only exist as a zig-zag? One will have to apply simplicial looping and both the unit and the counit of Ω⊣W¯\Omega \dashv \overline{W}. Somehow.

    • CommentRowNumber8.
    • CommentAuthorUlrik
    • CommentTimeJul 11th 2021

    Fill in proof in homotopy type theory. The proof itself is one line, but I added some reminders about how things are defined in HoTT. I think we have these things elsewhere, so it would be good to add some more links. Later.

    diff, v18, current

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeJul 11th 2021
    • (edited Jul 11th 2021)

    Thanks!!

    Allow me to make some edits as I read through it:

    • hyperlinked type, function type, type universe, Sigma-type …

      and ∞-group, ∞-action, adjointness …;

    • changed “object of type” to “term of type” (okay?!)

    • added hyperlink for “automorphism ∞-group”

    • expanded out “pointed map” to “morphism of pointed homotopy types”

    • changed “classifying” to “delooping” and changed “BGB G” to “BG\mathbf{B}G”, in accord with notation we have mostly been sticking to on the nnLab

      – you know the reason, but just to amplify for bystanders: it’s important that we are speaking here about the internal delooping (hence the universal moduli ∞\infty-stack) BG\mathbf{B}G instead of just the classifying space BGB G of GG, which, when a shape modality is present, is typically just the shape of the moduli stack BG≃ʃBGB G \simeq ʃ \mathbf{B}G

    • similarly, where the circle appears I replaced S 1S^1 with ʃS 1ʃ S^1 and made explicit that ʃS 1≃Bℤʃ S^1 \,\simeq\, \mathbf{B}\mathbb{Z}

      (this leaves room for future discussion here of the actual free loop stack which involves the actual circle S 1S^1)

    diff, v19, current

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeJul 11th 2021

    also I have added a line-break in the deduction

    G ad⫽G =∑ t:BG(t= BGt) ≃(ʃS 1→BG), \begin{aligned} G^{ad} \!\sslash\! G & \;=\; \sum_{t: \mathbf{B} G} (t =_{\mathbf{B} G} t) \\ & \;\simeq\; (ʃS^1 \to \mathbf{B} G), \end{aligned}

    to avoid the last two lines together to look like an identity type.

    diff, v19, current

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeJul 11th 2021
    • (edited Jul 11th 2021)

    Where the higher inductive type of the circle is mentioned, I have added a pointer to higher inductive type – examples – circle.

    I wish we had a page on the circle-HIT that would explain the conclusion being drawn here a little more…

    [ oh, I see we have a stub entry circle type. That has room to be expanded… ]

    diff, v19, current

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeJul 11th 2021
    • (edited Jul 11th 2021)

    Now I have a question on the logic of the derivation:

    It is clear that the function type ʃS 1→BGʃ S^1 \to \mathbf{B}G is the correct formalization of the free loop space (actually: intertia ∞\infty-stack) ΛBG\Lambda \mathbf{B}G. So, running your argument backwards, we find that this evident free loop type is equivalent to the action t:BG⊢(t= BGt):Typet \colon \mathbf{B}G \vdash (t =_{\mathbf{B}G} t) \,\colon\, Type. However, it is less “clear” that this action is the adjoint action. While I certainly don’t doubt it, I am wondering if this can be formally substantiated further in HoTT.

    Compare to the situation in the pseudocode formerly known as mathematics: There we also went ahead and defined ℒBG∈H /BG≃GActs(H)\mathcal{L} \mathbf{B}G \, \in \, \mathbf{H}_{/\mathbf{B}G} \simeq G Acts(\mathbf{H}) as being the adjoint action – and it’s certainly a good definition – but it takes a little bit of actual work (as per #1) to demonstrate that for a given ∞\infty-group GG this definition captures the actual defining formula

    G×G ⟶ G (g,h) ↦ h −1⋅g⋅h \array{ G \times G &\longrightarrow& G \\ (g,h) &\mapsto& h^{-1} \cdot g \cdot h }

    of the adjoint action.

    Do you see a way to prove, in HoTT, that this formula defines the type t:BG⊢(t= BGt):Typet \colon \mathbf{B}G \vdash (t =_{\mathbf{B}G} t) \colon Type ?

    • CommentRowNumber13.
    • CommentAuthorUlrik
    • CommentTimeJul 11th 2021

    Thanks for all the improvements: looks good!

    Do you see a way to prove, in HoTT, that this formula defines the type t:BG⊢(t= BGt):Typet \colon \mathbf{B}G \vdash (t =_{\mathbf{B}G} t) \colon Type ?

    No single formula concerning elements suffices to define an ∞\infty-action. You’d have to give all the higher coherences as well.

    But conversely, we can easily show that the family t↦(t= BGt)t \mapsto (t =_{\mathbf{B}G} t) acts on elements as we want. This is because transport in the identity family BG×BG→U\mathbf{B} G \times \mathbf{B} G \to U, (t,u)↦(t=u)(t,u) \mapsto (t=u), is by path pre/post-composition.

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeJul 11th 2021

    No single formula concerning elements suffices to define an ∞\infty-action. You’d have to give all the higher coherences as well.

    Externally it works: I gave the proof that in the model structure on simplicial sets, any abstractly defined adjoint ∞\infty-action is represented by a degree-wise adjoint action of simplicial groups. That’s the “folklore” that I set out to nail down when I started this thread.

    But conversely, we can easily show that the family

    Might you have energy left to add a paragraph demonstrating this? (I see what you are saying, but I’d rather you write it out to our readers than that I do.)

    • CommentRowNumber15.
    • CommentAuthorUlrik
    • CommentTimeJul 11th 2021

    Add a paragraph explaining transport in the adjoint action family.

    diff, v21, current

    • CommentRowNumber16.
    • CommentAuthorUlrik
    • CommentTimeJul 11th 2021

    Externally it works: I gave the proof that in the model structure on simplicial sets, any abstractly defined adjoint ∞\infty-action is represented by a degree-wise adjoint action of simplicial groups. That’s the “folklore” that I set out to nail down when I started this thread.

    Right. Also, we don’t know that we can’t define A ∞A_\infty objects in HoTT and thus prove all this internally, it’s just the usual story that we haven’t been able to so far.

    Might you have energy left to add a paragraph demonstrating this?

    Done. For transport I added a link to homotopy lifting property, even though that page doesn’t talk about type theory. Maybe there should rather be a section at dependent type that explains transports, dependent actions on paths, and stuff like that.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeJul 11th 2021

    Thanks!!

    Maybe there should rather be a section at dependent type that explains transports, dependent actions on paths, and stuff like that.

    It would be much appreciated if you’d have the further energy to add such a section!

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeJul 13th 2021
    • (edited Jul 13th 2021)

    By the way, I still feel there is something missing in the HoTT argument. Namely, currently the argument given is really to observe that it works for 1-groups and the suggestion that this is suggestive of the general case, since everything is so natural. But this was exactly the state of the “folklore” in the classical context, which this entry here hopes to improve on.

    Could one maybe generalize the HoTT argument at least to 2-groups, maybe in a way that makes it clear how on could induct up to nn-groups for any finite nn?

    • CommentRowNumber19.
    • CommentAuthorUlrik
    • CommentTimeJul 14th 2021

    By the way, I still feel there is something missing in the HoTT argument. Namely, currently the argument given is really to observe that it works for 1-groups and the suggestion that this is suggestive of the general case, since everything is so natural. But this was exactly the state of the “folklore” in the classical context, which this entry here hopes to improve on.

    I think this “gap” is currently better filled on the side of models, which is after all where we get the equivalence PtdConn(𝒳)≃Grp(𝒳)PtdConn(\mathcal{X}) \simeq Grp(\mathcal{X}) from. (Until we solve the coherence problem etc.) Might there be some place in the quasicategory literature/Lurie where its proven that under this equivalence GG with its adjoint action corresponds to the type family t↦(t=t)t \mapsto (t=t) (and GG with its translation action corresponds to the type family t↦(pt=t)t \mapsto (pt = t))?

    Could one maybe generalize the HoTT argument at least to 2-groups, maybe in a way that makes it clear how on could induct up to nn-groups for any finite nn?

    For 2-groups this should be possible. I’ll add it to my list of things to investigate!

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeJul 15th 2021

    Might there be some place in the quasicategory literature

    I’d be inclined to say that this is what the proof accomplishes that I recorded here. This together – if you wish – with your argument translating the free loop space into ∑ t:BG(t=t)\sum_{t \colon \mathbf{B}G} (t = t) (which, if we use external reasoning in the first place, does not even need HIT’s as the model-categorical semantics of ∑ t:BG(t=t)\sum_{t \colon \mathbf{B}G} (t = t) is the free loop space object right away).

    I guess my request to make this “more internal” may not be reasonable, but it grew out of the exchange we had in the other thread (startimg here).

    I’ll add it to my list of things to investigate!

    Okay, thanks! I’ll be interested.

    By the way, not to distract us too much, but what happened to Eric Finster’s claim to have solved the issue of higher coherent structures in HoTT? In principle? I understand there was a problem with the original argument, but then apparently arXiv:2105.00024 salvaged much of it. Or something like this, I haven’t been following.

    • CommentRowNumber21.
    • CommentAuthorUlrik
    • CommentTimeJul 15th 2021

    I’d be inclined to say that this is what the proof accomplishes that I recorded here.

    How hard would it be to generalize this argument to an arbitrary ∞-topos?

    (which, if we use external reasoning in the first place, does not even need HIT’s as the model-categorical semantics of ∑ t:BG(t=t)\sum_{t \colon \mathbf{B}G} (t = t) is the free loop space object right away).

    Right, this definition still uses a homotopy colimit description of S 1S^1 at the meta-level, so it’s related.

    I guess my request to make this “more internal” may not be reasonable, but it grew out of the exchange we had in the other thread (startimg here).

    As a counterpoint, in HoTT at the moment, we have to take PtdConnPtdConn as the definition of GrpGrp, and from this point of view, it’s equally natural to take t↦(t=t)t \mapsto (t=t) as the definition of the conjugation action. From first principles, I don’t see why that’s a worse definition than one in terms of simplicial objects.

    By the way, not to distract us too much, but what happened to Eric Finster’s claim to have solved the issue of higher coherent structures in HoTT? In principle? I understand there was a problem with the original argument, but then apparently arXiv:2105.00024 salvaged much of it. Or something like this, I haven’t been following.

    Yes, the original definition defines the wrong thing (at the level of associativity data, or maybe one level higher). The new work proposes an extension of type theory with a universe of polynomial monads. I’m not very familiar with it yet, it’s certainly promising, though it’s not clear that it completely solves the problem, and I don’t know if the meta-theory works out (homotopy canonicity, models in all ∞-toposes, etc, that remains to be seen, IIUC.)

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeNov 29th 2022
    • (edited Nov 29th 2022)

    I have fixed the label of the top left diagonal arrow in the diagram here.

    (previously the component in W𝒢W \mathcal{G} had an “h −1h^{-1}” which should have been an “hh”, but in addition an inverse factor of “g→\vec g” had been missing )

    diff, v23, current

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeNov 30th 2022
    • (edited Nov 30th 2022)

    I suppose that – for AA an abelian group and n∈ℕn \in \mathbb{N} – we have a retraction:

    id:B nA⟶Maps(Bℤ,B n+1A)⫽Bℤ⟶B nA id \;\; \colon \;\; \mathbf{B}^n A \longrightarrow Maps\big( \mathbf{B}\mathbb{Z},\; \mathbf{B}^{n+1}A \big) \sslash \mathbf{B}\mathbb{Z} \longrightarrow \mathbf{B}^n A

    Is that right? I can see it through a simplicial model for small nn, but right now I am lacking a transparent proof.

    The idea is to use the splitting

    Maps(Bℤ,B n+1A)≃B nA×B n+1A, Maps\big( \mathbf{B}\mathbb{Z},\; \mathbf{B}^{n+1}A \big) \;\; \simeq \;\; \mathbf{B}^n A \;\times\; \mathbf{B}^{n+1} A \,,

    where, intuitively, the first factor records based loops, and the second the position of their basepoint.

    Now Bℤ\mathbf{B}\mathbb{Z} acts on this by rotating the loops through full periods. This actually leaves the loops as such fixed, but it makes their basepoint run through the loop. In other words, the Bℤ\mathbf{B}\mathbb{Z}-action on this product may be understood as an action just on the B n+1A\mathbf{B}^{n+1}A-factor, but parameterized on the B nA\mathbf{B}^n A-factor. Therefore the latter projects out of the homotopy quotient

    id:B nA⟶(B nA×B n+1A)⫽Bℤ⟶B nA. id \;\; \colon \;\; \mathbf{B}^n A \longrightarrow \Big( \mathbf{B}^n A \,\times\, \mathbf{B}^{n+1}A \Big) \sslash \mathbf{B}\mathbb{Z} \longrightarrow \mathbf{B}^n A \,.

    That’s the intuition, anyway. I’d like a transparent proof of this,

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeNov 30th 2022

    addendum: A little rational homotopy theory (here) proves this statement at least for A=ℚA = \mathbb{Q} and thus also for A=ℤA = \mathbb{Z}.

1 to 24 of 24

  1.