For AA a monoid equipped with an action on an object VV, an invariant of the action is an element of VV which is taken by the action to itself, hence a fixed point for all the operations in the monoid.


A robust definition of invariants that generalizes to homotopy theory is via the expression of actions as action groupoids regarded as sitting over delooping groupoids, as discussed at infinity-action and at geometry of physics -- representations and associated bundles.

We describe how the ordinary concept of invariants is recovered from this perspective and then consdider its immediate generalizations to (infinity,1)-topos theory and its formalization in homotopy type theory.

Via sections of action groupoid projections


For GG a discrete group, ρ\rho a GG-action on some set SS, then the set of invariants of that action is equivalent to the groupoid of sections of the action groupoid projection of this proposition, corresponding to the action via this proposition.


The sections in question are diagrams in Grpd of the form

BG σ S//G id p ϕ BG, \array{ \mathbf{B}G && \stackrel{\sigma}{\longrightarrow} && S//G \\ & {}_{\mathllap{id}}\searrow &\swArrow_{\mathrlap{\simeq}}& \swarrow_{\mathrlap{p_\phi}} \\ && \mathbf{B}G } \,,

hence the groupoid which they form is equivalently the hom-groupoid

Grpd /BG(id BG,p ρ)Grpd Grpd_{/\mathbf{B}G}(id_{\mathbf{B}G}, p_\rho) \in Grpd

in the slice of Grpd over BG\mathbf{B}G. As in the proof of this proposition, with the fibrant presentation (p ρ) (p_\rho)_\bullet of this proposition, this is equivalently given by strictly commuting diagrams of the form

(BG) σ (S//G) id = (p ϕ) (BG) . \array{ (\mathbf{B}G)_\bullet && \stackrel{\sigma_\bullet}{\longrightarrow} && (S//G)_\bullet \\ & {}_{\mathllap{id_\bullet}}\searrow &=& \swarrow_{\mathrlap{(p_\phi)_\bullet}} \\ && (\mathbf{B}G)_\bullet } \,.

These σ\sigma now are manifestly functors that are the identiy on the group labels of the morphisms

σ :(* g *)(σ(*) g σ(*) =ρ(σ(*)(g))). \sigma_\bullet \;\colon\; \left( \array{ \ast \\ \downarrow^{\mathrlap{g}} \\ \ast } \right) \;\; \mapsto \;\; \left( \array{ \sigma(\ast) \\ \downarrow^{\mathrlap{g}} \\ \sigma(\ast) & = \rho(\sigma(\ast)(g)) } \right) \,.

This shows that they pick precisely those elements σ(*)S\sigma(\ast) \in S which are fixed by the GG-action ρ\rho.

Moreover, since these functors are identity on the group labels, there are no non-trivial natural isomorphisms between them, and hence the groupoid of sections is indeed a set, the set of invariant elements.

More generally, we may consider sections of these groupoid projections after pulling them back along some cocycle:


Given an associated bundle P× GVXP \times_G V\to X modulated, as in this proposition, by a morphism of smooth groupoids of the form g:XBGg \colon X \longrightarrow \mathbf{B}G, then its set of sections is equivalently the groupoid of diagrams

X σ S//G g p ϕ BG, \array{ X && \stackrel{\sigma}{\longrightarrow} && S//G \\ & {}_{\mathllap{g}}\searrow &\swArrow_{\mathrlap{\simeq}}& \swarrow_{\mathrlap{p_\phi}} \\ && \mathbf{B}G } \,,

hence the groupoid of sections is the slice hom-groupoid

Γ X(P× GV)Grpd /BG(g,p ρ). \Gamma_X(P\times_G V) \simeq Grpd_{/\mathbf{B}G}(g, p_\rho) \,.

By the defining universal property of the homotopy pullback in this proposition.


Taken together this means that invariants of group actions are equivalently the sections of the corresponding universal associated bundle.

Invariants of \infty-group actions

For H\mathbf{H} an (∞,1)-topos, GGrp(H)G \in Grp(\mathbf{H}) an ∞-group and

*:BG:V(*):Type * : \mathbf{B} G \vdash : V(*) : Type

an ∞-action of GG on VHV \in \mathbf{H}, the type of invariants is the absolute dependent product

*:BGV(*):Type. \vdash \prod_{* : \mathbf{B}G} V(*) : Type \,.

The connected components of this is equivalently the group cohomology of GG with coefficients in the infinity-module VV.

representation theory and equivariant cohomology in terms of (∞,1)-topos theory/homotopy type theory:

homotopy type theoryrepresentation theory
pointed connected context BG\mathbf{B}G∞-group GG
dependent type∞-action/∞-representation
dependent sum along BG*\mathbf{B}G \to \astcoinvariants/homotopy quotient
context extension along BG*\mathbf{B}G \to \asttrivial representation
dependent product along BG*\mathbf{B}G \to \asthomotopy invariants/∞-group cohomology
dependent product of internal hom along BG*\mathbf{B}G \to \astequivariant cohomology
dependent sum along BGBH\mathbf{B}G \to \mathbf{B}Hinduced representation
context extension along BGBH\mathbf{B}G \to \mathbf{B}H
dependent product along BGBH\mathbf{B}G \to \mathbf{B}Hcoinduced representation
spectrum object in context BG\mathbf{B}Gspectrum with G-action (naive G-spectrum)

Revised on January 4, 2016 09:58:27 by Urs Schreiber (