# Start a new discussion

## Not signed in

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

## Site Tag Cloud

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

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeJul 3rd 2021

am recording an actual proof that

$\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).

• 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 $L B G \simeq Ad(E G)$, Appendix A in String Topology of Classifying Spaces, 2007 (pdf)
• 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.

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeJul 4th 2021

• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeJul 4th 2021
• (edited Jul 10th 2021)

[ redundant ]

• CommentRowNumber7.
• 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

$\big[ \mathbf{B}\mathbb{Z}, \, \mathbf{B}\mathcal{A} \big] \;\; \simeq \;\; \mathcal{A} \times \mathbf{B}\mathcal{A} \,.$

and with the example

$\mathcal{L} \mathbf{B}^{n+1}A \;\simeq\; \mathbf{B}^n A \,\times\, \mathbf{B}^{n+1}A \,,$
• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeJul 9th 2021

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

I.e. for $\overline{W}\mathcal{G} \longrightarrow \overline{W}\mathcal{K}$ a morphism, do we have an induced morphism $\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 $\Omega \dashv \overline{W}$. Somehow.

• CommentRowNumber9.
• 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.

• CommentRowNumber10.
• 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

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

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

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

– 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) $\mathbf{B}G$ instead of just the classifying space $B G$ of $G$, which, when a shape modality is present, is typically just the shape of the moduli stack $B G \simeq ʃ \mathbf{B}G$

• similarly, where the circle appears I replaced $S^1$ with $ʃ S^1$ and made explicit that $ʃ 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^1$)

• CommentRowNumber11.
• CommentAuthorUrs
• CommentTimeJul 11th 2021

also I have added a line-break in the deduction

\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.

• CommentRowNumber12.
• 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… ]

• CommentRowNumber13.
• 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 \to \mathbf{B}G$ is the correct formalization of the free loop space (actually: intertia $\infty$-stack) $\Lambda \mathbf{B}G$. So, running your argument backwards, we find that this evident free loop type is equivalent to the action $t \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 $\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 $G$ this definition captures the actual defining formula

$\array{ G \times G &\longrightarrow& G \\ (g,h) &\mapsto& h^{-1} \cdot g \cdot h }$

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

• CommentRowNumber14.
• 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 \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 \mapsto (t =_{\mathbf{B}G} t)$ acts on elements as we want. This is because transport in the identity family $\mathbf{B} G \times \mathbf{B} G \to U$, $(t,u) \mapsto (t=u)$, is by path pre/post-composition.

• CommentRowNumber15.
• 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.)

• CommentRowNumber16.
• CommentAuthorUlrik
• CommentTimeJul 11th 2021

• CommentRowNumber17.
• 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_\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.

• CommentRowNumber18.
• 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!

• CommentRowNumber19.
• 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 $n$-groups for any finite $n$?

• CommentRowNumber20.
• 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(\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 $G$ with its adjoint action corresponds to the type family $t \mapsto (t=t)$ (and $G$ with its translation action corresponds to the type family $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 $n$-groups for any finite $n$?

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

• CommentRowNumber21.
• 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 $\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 $\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.

• CommentRowNumber22.
• 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 $\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^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 $PtdConn$ as the definition of $Grp$, and from this point of view, it’s equally natural to take $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.)