pointer (especially Part I):

- Severin Bunk, Carlos S. Shahbazi.
*Higher Geometric Structures on Manifolds and the Gauge Theory of Deligne Cohomology*(2023). (arXiv:2304.06633).

Not a mistake per se, it’s just that taking colimits in the type of groups doesn’t commute with taking elements, of course, but the notation can obscure that when we reuse the symbol for a group to denote its elements as well.

]]>On those points (1) and (2):

Thanks again. I’ll think about that tomorrow, as I am about to call it quits, too. Are you saying I have a mistake in (1)? Will think about it.

]]>Will do, first thing tomorrow, as it’s getting late here.

]]>Thanks!

…just note that…

Maybe you could add that to the entry, under “Proof – In homotopy type theory” ?

]]>A type-theory language account on these matters is, of course, in Buchholtz, van Doorn, Rijke’s arXiv:1802.04315. They briefly mention the conjugation action on p. 11, though they just seem to recall the folklore there.

I’m not sure what you mean by “just”. We point out many results that are trivial to establish in the context of HoTT, but we weren’t aware of any HoTT folklore around them, except for what was in Mike’s café blog post. This didn’t discuss the adjoint action nor semi-direct products.

We were short on space, so we couldn’t include many of the one-line proofs, unfortunately. (We chose to present the stabilization stuff in more detail, instead.)

For instance, to see that $G^{ad} \sslash G = L B G$, just note that

$G^{ad} \sslash G = \sum_{t : B G}(t = t) = (S^1 \to BG)$by the universal property of the circle as a HIT.

Looking at (1) and (2) from above in HoTT, we see that (1) holds if we take (b) as a definition: Suppose $\Gamma : B G \to \infty Grp$ is an $\infty$-group with a $G$-action, represented by $B \Gamma : B G \to U_*$, taking values in pointed connected types. Then $B \Gamma \sslash G = \sum_{t : B G} B \Gamma^t = B(G \ltimes \Gamma)$ is again pointed and connected, and the loop type is $\Omega(B \Gamma \sslash G) = \sum_{g : G} (trp^{B \Gamma}\,g\,* = *) = G \times \Gamma$, since we have a family of pointed types, so the transport of the point stays in place. (This represents the semi-direct product as you note.) We should be a bit careful, though, since the homotopy orbits of the type of elements of $\Gamma$ gives something different: $\Gamma \sslash G = \sum_{t : B G} \Gamma^t = \sum_{t : B G} (* =_{B \Gamma^t} *)$.

As to (2): this is exactly right, as a simple calculation shows (which I’ll skip here).

Finally, the claim that $Groups(\mathbf{H}_{/\mathbf{B}G})$ consists precisely of the above is clear from the HoTT point of view: If $\mathbf{H}$ is a model of HoTT, then so is $\mathbf{H}_{/\mathbf{B}G}$ for any $\infty$-group $G$ in $\mathbf{H}$, by simply prepending $x : B G$ to the context of all judgments. In particular, we interpret “pointed connected type” as a family of pointed connected types indexed by $B G$, which is what $\Gamma$ was above.

]]>So (1) and (2) is certainly correct, in that they do yield a sub-$\infty$-groupoid of $Groups(\mathbf{H}_{/\mathbf{B}G})$ and they do subsume the traditional external equivariant groups and equivariant bundles.

I just don’t know if they exhaust $Groups(\mathbf{H}_{/\mathbf{B}G})$. Hence I don’t know currently whether a “$G$-equivariant $\infty$-group” could be slightly more general than being a semidirect product $\infty$-group $\Gamma \rtimes G$. (It seems unlikely, but I don’t have a proof.)

I have re-installed the question on which I get stuck in the Sandbox.

So where for ordinary topological groups we have an equivalence

$\{semidirect\; products\;with\;G\} \xrightarrow{ \;\;\;\;\; \simeq \;\;\;\;\; } Groups(G Actions)$for $\infty$-groups I currently only know that this map is a full embedding.

This should be a minor technical issue, and not a big deal. If the map should really not be an equivalence, it would just mean that equivariant $\infty$-bundles could show a new structural phenomenon not seen in equivariant topological bundles. It feels like this is unlikely, though.

]]>Presumably whatever HoTT delivers is right, so then it’s a question of interpreting any HoTT-reasoning in whatever $(\infty, 1)$-topos. E.g., if we have the abstract general theory of $\Gamma$-principal bundles, then we just see what this amounts to in $\mathbf{H}_{/\mathbf{B} G}$.

So that’s the issue with (1) and (2), whether these are the correct externalization of principal bundle theory internal to a $(\infty, 1)$-topos of the kind $\mathbf{H}_{/\mathbf{B} G}$?

Hmm, what makes for externalization to be a non-trivial problem?

]]>Yes, absolutely. I had tried to have a discussion on this in a thread elsewhere.

So for $G$ any $\infty$-group, a “$G$-equivariant $\infty$-group” $\Gamma$ should be a group-object in the slice $\mathbf{H}_{/\mathbf{B}G}$. I still don’t quite understand these in full generality, but I understand the following sub-class:

Claim:

1) If $\Gamma$ is a group in $\mathbf{H}$ which is equipped with a $G$-action by group automorphisms, then (a) $\Gamma \sslash G \in Groups(\mathbf{H}_{/\mathbf{B}G})$ and (b) $\mathbf{B}(\Gamma \sslash G) \simeq (\mathbf{B}\Gamma) \sslash G$.

2) The $G$-equivariant $\infty$-groups of this form are equivalent to split $\infty$-group extensions in $\mathbf{H}$ of the form $\Gamma \overset{hofib}{\longrightarrow} \Gamma \rtimes G \to G$, under the identification $(\mathbf{B}\Gamma) \sslash G \simeq \mathbf{B}(\Gamma \rtimes G)$.

I think I have proof of these two statements (for what it’s worth, but it does require an argument that is not completely trivial, unless I am missing something).

Moreover, I can see that the general group object in $\mathbf{H}_{/\mathbf{B}G}$ is a structure very close to (1) and (2), but I still fail to see a proof that (1) and (2) exhaust the group objects in $\mathbf{H}_{/\mathbf{B}G}$.

In any case, once we have such a group object in the slice over $\mathbf{B}G$, then the $\infty$-groupoid of $G$-equivariant $\Gamma$-principal $\infty$-bundles on $G$-stacks $X \in \mathbf{H}_{/\mathbf{B}G}$ is

$G Equv \Gamma PrinBdls(\mathbf{H})_{X} \;=\; \mathbf{H}_{/\mathbf{B}G} \big( X \sslash G, \; \mathbf{B}(\Gamma \sslash G) \big)$For the cases in the class (1), (2), this subsumes the traditional notion of equivariant principal bundles, under the embedding $DTopologicalSpaces \xhookrightarrow{CDfflg} \mathbf{H} \coloneqq SmoothGroupoids_\infty$.

]]>If a type in $\mathbf{H}/\mathbf{B} G$ is a $G$ $\infty$-action, what’s a dependent type there, so $\ast : \mathbf{B} G, v: V(\ast) \vdash W(\ast, v): Type$? Does that amount to a kind of equivariant bundle?

So if $W$ is a principal bundle over $V$, then if all is in the context of $\mathbf{B} G$ that’s why the $\Gamma$ at equivariant principal bundle needs to be considered with a $G$-action?

]]>Well, he seems to be looking to understand the algebraic structure of dependent type theory syntax:

The fact that conjugation is an example of this structure is interesting, but it also means that the structure does not completely characterize dependent type syntax:

My suspicion is that conjugation is appearing as a case of internal-hom as a kind of exponential.

]]>I have followed the link now, but would need to have a closer look.

To see the conjugation action (or any action) naturally from homotopy type theory one needs at least homotopy 1-types, in order to have 0-truncated groups (at least) realized as $G \simeq \Omega \mathbf{B}G$. Does Spivak mean to consider this?

A type-theory language account on these matters is, of course, in Buchholtz, van Doorn, Rijke’s arXiv:1802.04315. They briefly mention the conjugation action on p. 11, though they just seem to recall the folklore there.

]]>I was pointing David Spivak to the adjoint action over here. I think that’s right about why conjugation appears as an example of his ’jump’ monad.

]]>cross-linked the example of the adjoint action (here) with *free loop space of a classifying space*

added publication data to:

- Matan Prezma,
*Homotopy normal maps*, Algebr. Geom. Topol. Volume 12, Number 2 (2012), 1211-1238. (arXiv:1011.4708, euclid:agt/1513715387)

added publication data to:

- Amit Sharma,
*On the homotopy theory of $G$-spaces*, International Journal of Mathematics and Statistics Invention, Volume7 Issue 2 (arXiv:1512.03698, published pdf)

Added an expositional section *Examples – Discrete group actions on sets* which spells out in detail how the general abstract slicing perspective recovers ordinary permutation representations.

I should maybe copy this also to, or at least link to also from, *action groupoid* and *permutation representation*.

I have now written this (linearization of $\infty$-actions) out in more detail in section 3.10.5 of dcct (pdf).

In section 3.10.11 I use this to axiomatize Cartan geometry in differential cohesion, via the key example (3.10.45) of the canonical linearized $H$ action on $\mathfrak{g}/\mathfrak{h}$ .

(I have been fiddling with the axiomatization of Cartan geometry in homotopy-type theory a bit, as you may recall. My first versions were not so good, but I think now I am converging.)

]]>There is a nice formalization of linearization of $\infty$-actions in axiomatics of differential cohesion. I have added it to the entry here.

(The text deserves further polishing, but I am in a haste now as my battery is dying.)

]]>added a little observation – here – on how the automorphism action on an object in a slice is given by descending the corresponding map to the homotopy quotient of the induced action on the dependent sum.

(This innocent statement gives symplectic reduction for prequantum n-bundles)

]]>added now also a new section *References – For actions of topological groups* with the following text (which might also go into a Properties-section, admittedly):

[ text extracted from entry ]

That $G$-actions for $G$ a topological group in the sense of G-spaces in equivariant homotopy theory (and hence with $G$ *not* regarded as the geometrically discrete ∞-group of its underying homotopy type ) are equivalently objects in the slice (∞,1)-topos over $\mathbf{B}G$ is Elmendorf’s theorem together with the fact, highlighted in this context in

- {#Rezk14} Charles Rezk,
*Global Homotopy Theory and Cohesion*, 2014

that

$G Space \simeq PSh_\infty(Orb_G) \simeq PSh_\infty(Orb_{/\mathbf{B}G}) \simeq PSh_\infty(Orb)_{/\mathbf{B}G}$is therefore the slice of the $\infty$-topos over the slice of the global orbit category over $\mathbf{B}G$.

!include equivariant homotopy theory – table

See at *equivariant homotopy theory* for more references along these lines.

…

]]>added to *infinity-action* under a new section *References – For discrete geometry* pointers to articles that discuss $G Act_\infty \simeq \infty Grpd_{/ B G}$.

(copied the same also to the end of the citations at *principal infinity-bundle*).

Added at *infinity-action* brief remarks in new subsections

This is more to remind myself to come back to it later. No time right now.

]]>