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.