equivalences in/of $(\infty,1)$-categories
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
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
Let $\mathcal{C}$ be an (∞,1)-category. Let $X \in \mathcal{C}$ be an object.
As a discrete ∞-group the automorphism $\infty$-group of $X$ is the sub-∞-groupoid
of the derived hom space of morphisms in $\mathcal{C}$ from $X$ to itself, on those that are equivalences.
Let $\mathcal{C}$ be a cartesian closed (∞,1)-category (for instance an (∞,1)-topos). Write
for the internal hom. Then for $X \in \mathcal{C}$ an object, the internal automorphism $\infty$-group is the subobject
of the internal hom on those morphism that are equivalences.
In the special case that $\mathcal{C}$ is an ∞-topos, the delooping $\mathbf{B}\mathbf{Aut}(X)$ of the internal automorphism $\infty$-group is equivalently the ∞-image
of the morphism
to the object classifier, that modulates $X$ (the “name” of $X$).
Let $\mathcal{C}$ be an (∞,1)-topos. Then its internal language is homotopy type theory. In terms of this the object $X \in \mathcal{C}$ is a type (homotopy type). In the type theory syntax the internal automorphism $\infty$-group $\mathbf{Aut}(X)$ then is (as a type, without yet the group structure)
the subtype of the function type on the equivalences. Its delooping $\mathbf{B}\mathbf{Aut}(X)$ is
where on the right we have the dependent sum over one argument of the bracket type/(-1)-truncation $[X = Y] = isInhab(X = Y)$ of the identity type $(X = Y)$.
The equivalence of this definition to the previous one is essentially equivalent to the univalence axiom.
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.
For $G \in \infty Grp(\mathcal{X})$ an ∞-group there is the direct automorphism $\infty$-group $Aut(G)$. But there is also the delooping $\mathbf{B}G \in \mathcal{X}$ and its automorphism $\infty$-group.
Sometimes (for instance in the discussion of ∞-gerbes) one considers
and calls this the automorphism $\infty$-group of $G$.
For instance when $G$ is an ordinary group, $AUT(G)$ is the 2-group discussed at automorphism 2-group.
There may be the structure of an ∞-Lie group on $Aut(F)$. The corresponding ∞-Lie algebra is an automorphism ∞-Lie algebra.
automorphism group, automorphism 2-group, automorphism $\infty$-group,
outer automorphism group, automorphism 2-group, outer automorphism ∞-group