Yeah, that’s the thing, it looks a little mixed:

In singular-cohesive HTT it’s the combination of

the geometric fixed locus operation $Maps\big( \prec \mathbf{B}G,\, \prec(-) \big)_{\prec \mathbf{B}G}$ on the group,

the naive quotient modality $\lt (-)$ on the object it acts on.

It’s not something I would have thought of on abstract grounds, and I haven’t even tried to think about in which abstract generality this works.

But now that I am seeing this one example I feel like there may be more to this (namely I am looking at the canonical $\mathbb{Z}_2$-equivariant action of $SU(3)$ on $\mathbb{C}P^2$. Applying this construction and using the AKM-theorem makes this reduce to an $SO(3)$-action on $S^4$. Still need to check if it’s the canonical $SO(3)$-action at that, but I guess it can’t be anything else…)

]]>How does this look in HoTT in terms of contexts $B G$, $B \Gamma$, dependent product for fixed point, truncation of dependent sum for naive quotient, etc.?

]]>If a $G$-equivariant group $\Gamma$ acts on a $G$-space $X$ (i.e. a group action internal to $G$-spaces), then the action does not generally pass to naive quotients – but:

The fixed locus $\Gamma^G$ does canonically act on the naive quotient $X/G$ (essentially since reflexive coequalizers commute with products).

Elementary as this is, I seem to have run into amusing example for this situation; now I am wondering if this should be thought of as an example of something that is relevant more generally.

]]>I have put my thoughts so far into the Sandbox (involves `tikz`

, so doesn’t render here).

[ … ]

]]>Now finally turning to the abstract $\infty$-topos theoretic perspective on these matters:

Let

$\mathbf{H}$ be an $\infty$-topos,

$G \in Groups(\mathbf{H})$

then Prop. 2.102 on p. 35 of our *Proper Orbifold Cohomology* shows that its homotopy quotient by its group-automorphism group is itself, canonically, a group object in the slice

I expect the converse is true:

Conjecture. *For $K$ a group in $\mathbf{H}$, group objects in $\mathbf{H}_{/\mathbf{B}K}$ are equivalent to group objects in $\mathbf{H}$ that are equipped with actions by K via group automorphisms*.

But I don’t have a proof of this converse statement yet.

]]>I won’t be editing that entry for the moment. But, yes, as in #5, differential cohomology in a singular-cohesive $\infty$-topos gives equivariant $\infty$-connections on equivariant $\infty$-bundles.

(With the usual caveats: Abelian connections come out on the nose from a Hopkins-Singer style homotopy pullback along a character map, while non-abelian connections come out subject to more identifications, unless one intervenes by hand and uses more properties of a concrete ambient model.)

]]>Presumably equivariant connection could be given a similar internalised treatment.

]]>That’s certainly what I am really after behind the scenes:

Question: What’s a twist in twisted equivariant (differential) $A$-cohomology?

Answer: it’s an $A$-fiber $\infty$-bundle internal to a singular-cohesive $\infty$-topos. Of course.

Question: What kind of topological bundles with bells-and-whistles present these under passage to shape?

Answer: Principal bundles internal to $G$-spaces – hence tomDieck69-bundles.

But yeah, it is weird that it takes an undergrad-level entry *equivariant group* to fill a gap in the literature.
Some 20th century maths has fallen into the 21st century here and needs to be cleaned up now ;-)

Strange that internalisation hasn’t been rolled out here before. Presumably it’s what follows from a HoTT rendition in equivariant context.

]]>some last polishing. Now I have had enough of this.

]]>Now some content in place, spelling out how

groups internal to $G$-spaces are equivalently semidirect products with $G$;

group actions internal to $G$-spaces are equivalently actions of these semidirect product groups.

All elementary and essentially trivial, but spelled out, hereby, nonetheless.

]]>starting something, to go with and rhyme on *equivariant principal bundle*. Not done yet, but need to save.