Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
am recording an actual proof that
ℒ(ˉW𝒢)≃𝒢ad⫽𝒢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).
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.
added pointer to the relevant 3 pages in
added pointer to
Does anyone know or see how to make the simplicial presentation in the entry here functorial in ˉW𝒢?
I.e. for ˉW𝒢⟶ˉW𝒦 a morphism, do we have an induced morphism (W𝒢×𝒢ad)/𝒢⟶(W𝒦×𝒦ad)/𝒦 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. Somehow.
Thanks!!
Allow me to make some edits as I read through it:
hyperlinked type, function type, type universe, Sigma-type …
and ∞-group, ∞-action, adjointness …;
added hyperlink for “automorphism ∞-group”
expanded out “pointed map” to “morphism of pointed homotopy types”
changed “classifying” to “delooping” and changed “BG” to “BG”, in accord with notation we have mostly been sticking to on the nLab
– 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 ∞-stack) BG instead of just the classifying space BG of G, which, when a shape modality is present, is typically just the shape of the moduli stack BG≃ʃBG
similarly, where the circle appears I replaced S1 with ʃS1 and made explicit that ʃS1≃Bℤ
(this leaves room for future discussion here of the actual free loop stack which involves the actual circle S1)
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… ]
Now I have a question on the logic of the derivation:
It is clear that the function type ʃS1→BG is the correct formalization of the free loop space (actually: intertia ∞-stack) ΛBG. So, running your argument backwards, we find that this evident free loop type is equivalent to the action t:BG⊢(t=BGt):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) 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 ∞-group G this definition captures the actual defining formula
G×G⟶G(g,h)↦h−1⋅g⋅hof the adjoint action.
Do you see a way to prove, in HoTT, that this formula defines the type t:BG⊢(t=BGt):Type ?
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):Type ?
No single formula concerning elements suffices to define an ∞-action. You’d have to give all the higher coherences as well.
But conversely, we can easily show that the family t↦(t=BGt) acts on elements as we want. This is because transport in the identity family BG×BG→U, (t,u)↦(t=u), is by path pre/post-composition.
No single formula concerning elements suffices to define an ∞-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 ∞-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.)
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∞ 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.
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!
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 n-groups for any finite n?
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(𝒳) 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 G with its adjoint action corresponds to the type family t↦(t=t) (and G with its translation action corresponds to the type family t↦(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 n-groups for any finite n?
For 2-groups this should be possible. I’ll add it to my list of things to investigate!
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) (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) 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.
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) is the free loop space object right away).
Right, this definition still uses a homotopy colimit description of S1 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 PtdConn as the definition of Grp, and from this point of view, it’s equally natural to take t↦(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.)
I suppose that – for A an abelian group and n∈ℕ – we have a retraction:
id:BnA⟶Maps(Bℤ,Bn+1A)⫽Bℤ⟶BnAIs that right? I can see it through a simplicial model for small n, but right now I am lacking a transparent proof.
The idea is to use the splitting
Maps(Bℤ,Bn+1A)≃BnA×Bn+1A,where, intuitively, the first factor records based loops, and the second the position of their basepoint.
Now Bℤ 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ℤ-action on this product may be understood as an action just on the Bn+1A-factor, but parameterized on the BnA-factor. Therefore the latter projects out of the homotopy quotient
id:BnA⟶(BnA×Bn+1A)⫽Bℤ⟶BnA.That’s the intuition, anyway. I’d like a transparent proof of this,
addendum: A little rational homotopy theory (here) proves this statement at least for A=ℚ and thus also for A=ℤ.
1 to 24 of 24