Paths and cylinders
Let be an (∞,1)-category. Let be an object.
As a discrete ∞-group the automorphism -group of is the sub-∞-groupoid
of the derived hom space of morphisms in from to itself, on those that are equivalences.
This is an ∞-group in ∞Grpd,
Let be a cartesian closed (∞,1)-category (for instance an (∞,1)-topos). Write
for the internal hom. Then for an object, the internal automorphism -group is the subobject
of the internal hom on those morphism that are equivalences.
In the special case that is an ∞-topos, the delooping of the internal automorphism -group is equivalently the ∞-image
of the morphism
to the object classifier, that modulates (the “name” of ).
In the syntax of homotopy type theory
Let be an (∞,1)-topos. Then its internal language is homotopy type theory. In terms of this the object is a type (homotopy type). In the type theory syntax the internal automorphism -group then is (as a type, without yet the group structure)
the subtype of the function type on the equivalences. Its delooping is
where on the right we have dependent sum over one argument of the bracket type/(-1)-truncation of the identity type .
The equivalence of this definition to the previous one is essentially equivalent to the univalence axiom.
In a 1-category
If happens to be a 1-category then the external automorphism -group of an object is the ordinary automorphism group of that object.
If happens to be a 1-topos, then the internal automorphism -group is the traditional automorphism group object in the topos. Etc.
For an ∞-group there is the direct automorphism -group . But there is also the delooping and its automorphism -group.
Sometimes (for instance in the discussion of ∞-gerbes) one considers
and calls this the automorphism -group of .
For instance when is an ordinary group, is the 2-group discussed at automorphism 2-group.
There may be the structure of an ∞-Lie group on . The corresponding ∞-Lie algebra is an automorphism ∞-Lie algebra.