automorphism infinity-group


(,1)(\infty,1)-Category theory

Homotopy theory

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed

models: topological, simplicial, localic, …

see also algebraic topology



Paths and cylinders

Homotopy groups

Basic facts





Let 𝒞\mathcal{C} be an (∞,1)-category. Let X𝒞X \in \mathcal{C} be an object.

As a discrete ∞-group the automorphism \infty-group of XX is the sub-∞-groupoid

Aut(X)𝒞(X,X) Aut(X) \hookrightarrow \mathcal{C}(X,X)

of the derived hom space of morphisms in 𝒞\mathcal{C} from XX to itself, on those that are equivalences.

This is an ∞-group in ∞Grpd,

Aut(X)Grp(Grpd). Aut(X)\in Grp(\infty Grpd) \,.


Let 𝒞\mathcal{C} be a cartesian closed (∞,1)-category (for instance an (∞,1)-topos). Write

[,]:𝒞 op×𝒞𝒞 [-,-] : \mathcal{C}^{op} \times \mathcal{C} \to \mathcal{C}

for the internal hom. Then for X𝒞X \in \mathcal{C} an object, the internal automorphism \infty-group is the subobject

Aut(X)[X,X] \mathbf{Aut}(X) \hookrightarrow [X,X]

of the internal hom on those morphism that are equivalences.

In the special case that 𝒞\mathcal{C} is an ∞-topos, the delooping BAut(X)\mathbf{B}\mathbf{Aut}(X) of the internal automorphism \infty-group is equivalently the ∞-image

*BAut(X)Obj * \to \mathbf{B}\mathbf{Aut}(X) \hookrightarrow Obj

of the morphism

*XObj * \stackrel{\vdash X}{\to} Obj

to the object classifier, that modulates XX (the “name” of XX).

In homotopy type theory

Let 𝒞\mathcal{C} be an (∞,1)-topos. Then its internal language is homotopy type theory. In terms of this the object X𝒞X \in \mathcal{C} is a type (homotopy type). In the type theory syntax the internal automorphism \infty-group Aut(X)\mathbf{Aut}(X) then is (as a type, without yet the group structure)

(XX):Type, \vdash (X \stackrel{\simeq}{\to} X) : Type \,,

the subtype of the function type on the equivalences. Its delooping BAut(X)\mathbf{B}\mathbf{Aut}(X) is

( Y:Type[Y=X]):Type, \vdash \; \left(\sum_{Y : Type} [Y = X]\right) \colon Type \,,

where on the right we have the dependent sum over one argument of the bracket type/(-1)-truncation [X=Y]=isInhab(X=Y)[X = Y] = isInhab(X = Y) of the identity type (X=Y)(X = Y).

The equivalence of this definition to the previous one is essentially equivalent to the univalence axiom.


In a 1-category

If 𝒞\mathcal{C} happens to be a 1-category then the external automorphism \infty-group of an object is the ordinary automorphism group of that object.

If 𝒞\mathcal{C} happens to be a 1-topos, then the internal automorphism \infty-group is the traditional automorphism group object in the topos. Etc.

Of \infty-groups

For GGrp(𝒳)G \in \infty Grp(\mathcal{X}) an ∞-group there is the direct automorphism \infty-group Aut(G)Aut(G). But there is also the delooping BG𝒳\mathbf{B}G \in \mathcal{X} and its automorphism \infty-group.

Sometimes (for instance in the discussion of ∞-gerbes) one considers

AUT(G):=Aut(BG) AUT(G) := Aut(\mathbf{B}G)

and calls this the automorphism \infty-group of GG.

For instance when GG is an ordinary group, AUT(G)AUT(G) is the 2-group discussed at automorphism 2-group.

There may be the structure of an ∞-Lie group on Aut(F)Aut(F). The corresponding ∞-Lie algebra is an automorphism ∞-Lie algebra.

Revised on May 4, 2016 12:40:05 by Urs Schreiber (