HIGHER SCHREIER THEORY IN CUBICAL AGDA

Abstract

Homotopy type theory (HoTT) enables reasoning about groups directly as the types of symmetries (automorphisms) of mathematical structures. The HoTT approach to groups—first put forward by Buchholtz, van Doorn, and Rijke—identifies a group with the type of objects of which it is the symmetries. This type is called the “delooping” of the group, taking a term from algebraic topology. This approach naturally extends the group theory to higher groups which have symmetries between symmetries, and so on. In this paper, we formulate and prove a higher version of Schreier’s classification of all group extensions of a given group. Specifically, we prove that extensions of a group G by a group K are classified by actions of G on a delooping of K. Our proof is formalized in Cubical Agda, a dependently typed programming language and proof assistant which implements HoTT.

1 Introduction

An extension of a group G by a group K is a short exact sequence

$$\begin{align*}0 \to K \xrightarrow{i} E \xrightarrow{p} G \to 0. \end{align*}$$

That is, a sequence of homomorphisms in which i is injective, p is surjective, and $\operatorname {{\mathrm {im}}} i = \ker p$ . As a set, any extension E is bijective with the cartesian product $K \times G$ ; but there may be many different group structures on this cartesian product which are, in some sense, built out of the group structures of G and K. Two extensions E and $E'$ are isomorphic when there is an isomorphism $E \cong E'$ commuting with the inclusions i and projections p; we define $\mathrm {{Ext}}(G, K)$ to be set of isomorphism classes of extensions of G by K.

In 1926 [27], Otto Schreier gave a series of cocycle conditions which classified all the possible extensions E of G by K. In doing so, he inaugurated the field of Schreier theory: the study of extensions of algebraic structures, and in particular of group-like structures. In 1934, Baer [6] examined the abelian extensions of abelian groups in terms of presentations of G by generators and relations, and discovered an abelian group law on $\mathrm {{Ext}}(G, K)$ . While working on computing Baer groups, Eilenberg, and Mac Lane noticed a similarity between those computations and the ones done in the cohomology of spaces. In a series of three papers [13–15], they developed a cohomology theory for groups and showed that $H^2(G; K)$ classified central extensions of G by an abelian group K—those extensions for which K lies in the center $ZG$ of G. They also related group cohomology to the cohomology of spaces by developing the Eilenberg–Mac Lane spaces $\mathsf {K}(G, n)$ , and showing that $H^2(G; K)$ , and hence central extensions, were in bijection with homotopy classes of pointed maps $\mathsf {K}(G, 1) \to _* \mathsf {K}(K, 2)$ .

This leads naturally to the following question: is there an object associated with a group K which classifies all extensions by a possibly non-abelian K? Building on work on non-abelian cohomology by Dedecker and Luks [11, 12], Grothendieck answered this question affirmatively with his Grothendieck construction [17], showing that there is a 2-group so that pseudo-functors from a delooping of G to correspond to extensions of G by K. This result was extended to stacks by Giraud [16] and to stacks of 2-groups by Breen [8].

In this paper, we will extend this classification of extensions to all (stacks of) higher groups [9] with an elementary and surprisingly concrete proof in homotopy type theory (HoTT).

Theorem 1.1 (Higher Schreier theorem)

For any higher groups G and K, the type $\mathrm {{EXT}}(G;K)$ of extensions of G by K is equivalent to the type of pointed functions , or, in other words, the type of actions of G on a delooping of K.

This result was first proved informally in [26]; here, we present a formal proof of the higher Schreier theorem in Cubical Agda [31]. It straightforwardly generalizes the elementary classification of split extensions by homomorphic actions of G on K familiar from any undergraduate textbook on group theory.

While Schreier’s original classification was concrete in the sense that it gave explicit cocycle conditions determining the group law of the extension, our construction is concrete in that it directly defines a type of mathematical structures whose group of symmetries gives the extension. We are able to do this by working in HoTT, where any object comes naturally equipped with a notion of identification—equality, isomorphism, structure-preserving equivalence, etc.—so that groups may be viewed as the self-identifications or symmetries of a object natively. Rather than expressing the group law of an extension E decomposes into the group laws of G and K via cocycles, Theorem 1.1 shows how the structures whose symmetries form the group E decompose into structures that whose symmetries form the group G and K, respectively.

As an example of this way of thinking, consider the short exact sequence

$$\begin{align*}0 \to \mathbb{R}^4 \to \mbox{Poincar}\acute{\rm e} \to \mbox{Lorentz} \to 0 \end{align*}$$

witnessing the Poincaré group as an extension of the Lorentz group by the group of translational symmetries of Minskowski space. We will see this series of group homomorphisms as the action on symmetries of a fiber sequence of types:

$$\begin{align*}\mathrm{{Affine}}(\mathbb{R}^4) \to \mathrm{{MinkowskiSpace}} \to \mathrm{{LorentzSpace}} \end{align*}$$

where $\mathrm {{Affine}}(\mathbb {R}^4)$ is the type of $4$ -dimensional real affine spaces, $\mathrm {{LorentzSpace}}$ is the type of Lorentz spaces (an $4$ -dimensional real vector space with an inner product of signature $3 + 1$ ), and $\mathrm {{MinkowskiSpace}}$ is the type of Minkowski spaces (an affine space over a Lorentz space, as defined for example in [29, p. 231]); the first function considers the real affine space as an affine space over the canonical Lorentz space $\mathbb {R}^{3 + 1}$ , and the second projects out the underlying Lorentz space. The corresponding classifying map determined by the higher Schreier theorem sends a Lorentz space V to the type $\mathrm {{Affine}}(V)$ of affine spaces over V; this evidently sends $\mathbb {R}^{3 + 1}$ to $\mathrm {{Affine}}(\mathbb {R}^4)$ .

In Section 2, we give a quick introduction to Cubical Agda, the dependently typed programming language in which our results are formalized. After that, in Section 3 we recall the theory of higher groups in HoTT. With this under our belt, we make short work of our main theorem in Section 4; in Section 6 we show how it generalizes the usual classification of split extensions by homomorphic actions.

2 A brief introduction to homotopy type theory and Cubical Agda

HoTT [30] is a novel foundation of mathematics based on Martin–Löf dependent type theory (MLTT) [23] with inspiration from modern homotopy theory. Through its basis in intuitionistic type theory, HoTT gives a computational perspective on mathematical proofs: proofs may be seen as programs that compute witnesses to the truth of a proposition. HoTT emerged from the work of Awodey and Warren [5] and Voevodsky [32] on the homotopical interpretation of MLTT, extending Hoffman and Streicher’s groupoid model of MLTT [18].

In type theory, there are four primitive judgements: that something is a type (denoted ), that something is an element of a type (denoted $a : A$ ), that two types are equal by definition (denoted $A := B$ ) and that two elements are equal by definition (denoted $a := b$ ). Formally, type theory is a system for moving from some constellation of these judgements to others via given rules. For example, if we judge A to be a type and for a free variable $x : A$ , we judge $B(x)$ to be a type, then we may judge ${(x : A)}\to B(x)$ and to be types. The former is the type of functions, and the latter the type of pairs. We define functions $f : {(x : A)}\to B(x)$ by lambda-abstraction: if $b(x) : B(x)$ for a free variable of type $x : A$ , then we judge . We use functions by applying them: if $a : A$ and $f : {(x : A)}\to B(x)$ , then $f(a) : B(a)$ , and we take the and . Similarly, if $a : A$ and $b : B(a)$ , we judge , and if then and ; to these we add the defininitional equalities , , and .

HoTT extends MLTT with a notion of path and an interpretation of types as homotopy types. In [5], Awodey and Warren interpret types as Kan complexes and elements as simplicial maps (or, more generally, objects and morphisms of a Quillen model category). This is the evident sense in which HoTT gains a homotopy interpretation; but it’s worth noting that this model also shows us how HoTT gives us tools for working directly with mathematical structures up to their appropriate notion of equivalence. Kan complexes include not only the singular complexes of topological spaces (their “homotopy types”, when considered up to equivalence in the Kan–Quillen model structure), but also the nerves of groupoids of mathematical structures. In the nerve of a groupoid, a path is an isomorphism. By Grothendieck’s homotopy hypothesis, Kan complexes are models of $\infty $ -groupoids—collections of higher mathematical structures, their equivalences, the equivalences between their equivalences, and so on. Moreover, Lumsdaine [21] and van den Berg and Garner [7] showed that Martin–Löf identity types endow types in MLTT with the structure of (appropriately weak) $\infty $ -groupoids.

Voevodsky’s univalence principle, which states that paths in type universes are equivalently equivalences between types, allows us to internalize this understanding of homotopy types as higher groupoids of mathematical structures to some extent. The first set-theoretic model for univalent type universes was put forward by Voevodsky and completed by Kapulkin and Lumsdaine [19], interpreting type universes as certain object classifiers in the Kan–Quillen model structure on simplicial sets. We will return to this point later in this introduction; for more on the structural interpretation of HoTT, see [4].

In [28], Shulman shows that HoTT can be interpreted in any $\infty $ -topos. When interpreted in appropriate $\infty $ -toposes (such as stacks on the site of continuous manifolds, as in ibid.), $\infty $ -groups are interpreted as stacks of $\infty $ -groups and their deloopings are interpreted as moduli stacks for principal bundles. In this way, we will be able to deduce a Schreier theorem for all stacks, and not just for homotopy types of spaces.

Agda is a dependently typed programming language based on MLTT in which both programs and proofs concerning the behavior of those programs are given by elements of types. Cubical Agda extends Agda with an abstract axiomatization of the unit interval $[0, 1] \subseteq \mathbb {R}$ and a number of basic operations concerning this interval suitable for doing synthetic homotopy theory in the resulting type theory. See [31] for a more comprehensive introduction to the type theory (originally put forward in [10]), [3] for use in the representation independence of data structures, and [24, 25] for synthetic homotopy theory done in Cubical Agda.

In particular, has “endpoints” , a “minimum” function , a “maximum” function , and a “reversal” (meant to resemble the function $x \mapsto 1 - x$ on the unit interval) which together equip with the structure of a de Morgan algebra.

A path in Cubical Agda is a function out of the interval whose value on the endpoints ${\mathsf {i0}}$ and ${\mathsf {i1}}$ is known by definition. If $a, b : A$ are elements, then elements of the path type may be defined by $\lambda $ -abstraction just like functions:

except that $p({\mathsf {i0}}) := a$ and $p({\mathsf {i1}}) := b$ by definition. If is a type family varying over the interval, then we also have a type of paths lying over this path of types, where $a : A\, {\mathsf {i0}}$ and $b : A\, {\mathsf {i1}}$ .

Paths act as an equality predicate in Cubical Agda. For example, we always have a reflexivity term

for any $a : A$ , as well as symmetry

Transitivity may be proven using another primitive notion: homogenous composition or $\mathsf {hcomp}$ . We will not go into any detail on how $\mathsf {hcomp}$ is used here to avoid a digression on partial elements; see [31] for more details. All we will need to know is that $\mathsf {hcomp}$ gives us a way to “cap off” open boxes, as in the following definition of conjugation of a path by paths and :

As a special case of conjugation, we get we get transitivity or path composition as . For those familiar with combinatorial homotopy theory, one can think of $\mathsf {hcomp}$ as a Kan-filling operation.

We can prove equations between paths by constructing paths in types of paths; since a path is a function , a path between paths is a function of two interval variables. It is this feature that gives cubical type theory the name; general terms may depend on many interval variables $i,\, j,\, k$ which can be thought of as varying over a “cube ”. We can in particular give paths and and the others needed to show that path composition is unital, invertible, and associative.

With this notion of path, we can define equivalences between types as functions having contractible fibers, following the definition given in the HoTT Book [30].

Definition 2.1. Let $f : A \to B$ be a map and $b : B$ . The fiber of f over b is the type of elements $a : A$ equipped with a path from $f(a)$ to b:

Definition 2.2. A type A is contractible if when it has a center of contraction $c : A$ and a path from every $x : A$ to c:

A function $f : A \to B$ is an equivalence if its fibers are contractible:

We denote the type of equivalences by :

Since paths are our only form of equality or identification in Cubical Agda, we may think of contractibility as unique existence. The principle of unique choice may be understood as the first projection from the type of pairs to A.

Since paths are functions, it is easy to compute path spaces in pair types :

Similarly, it is easy to compute paths in function types $\Sigma {[x : A]} B(x)$ , giving a form of function extensionality:

Type universes should be types as well, and this means that they should implement $\mathsf {hcomp}$ for paths (they should be fibrant). But what should paths of types be, and how should we compose them? Cubical Agda is univalent: paths of types correspond to equivalences between them. This is accomplished through another primitive notion: glue types $\mathsf {Glue}$ . Glue types work like $\mathsf {hcomp}$ in that they can “cap off” open boxes of types, but where the base of such a box is a path and the walls are equivalences:

By gluing the reflexive path onto an equivalence, we get Voevodsky’s univalence principle: paths between types are equivalences:

With glue types and univalence, we can construct paths between types by constructing equivalences between them; composition of paths corresponds to composition of their corresponding equivalences. In particular, the type of loops starting and ending at a type A is equivalent to the type of automorphisms of A.

Being contractible is a property of types, and being an equivalence is a property of functions. In type theory, propositions are represented as types, a practice known as propositions as types. The judgement $a : A$ can mean that a is a mathematical object of type A and also that a is a witness to the truth of the proposition A. We summarize the different viewpoints of the HoTT operations in Table 1.

Table 1 Correspondence between type theory, logic, sets, and homotopy theory.

As with other dependently typed languages, in Cubical Agda propositions are themselves expressed as types. However, following practice in HoTT [30], we do not consider all types to be propositions—some types are sets, like $\mathbb {N}$ , and some are types of mathematical structures, like the type of groups, for example. We identify the propositions as those types that have at most one element.

Definition 2.3. A type A is a proposition when for any two elements $a,\, b : A$ , the type of paths between them is contractible:

If is a family of propositions (that is, for all $a : A$ , ), then the pair type acts as the subtype of A consisting of those elements which satisfy P. By the computation of paths in pair types and the fact that paths in propositions are trivial, paths in subtypes may be computed in the underlying type:

Cubical Agda has higher inductive types (HITs), or inductive types with path constructors as well as term constructors. We may define the propositional truncation or squash type given by the following recursive HIT:

Giving an element of proves the proposition that there is some element of A, though there is not in general a function which lets us extract a specific witness. Propositional truncation therefore acts as an existential quantifier in cubical Agda: asserts that there exists an element of A, though it does not provide a specific witness to that existence.

Following the HoTT Book [30], we may define a type A to be a set if the path types in A are propositions:

Thinking of paths as equality predicates, this means that a set is a type in which equality is a proposition, as it usually considered to be.

With the type constructors so far described, we can now give an example of a type of mathematical structures. If G is a group, then we can define the type of left G-torsors (left G actions which are free, transitive, and inhabited) as follows:

Since paths in pairs may be computed componentwise, and since paths in propositions may be ignored (and types of paths in sets are propositions), we can compute that the type of paths is equivalent to the type of G-equivariant isomorphisms between T and $T'$ . Generally speaking, the structure identity principle (SIP) (see, e.g., [1]) guarantees that paths in types of mathematical structures correspond to structure-preserving equivalences In particular, the type of loops on G considered as a torsor over itself by left multiplication is equivalent to the type of G-equivariant automorphisms of G, which is equivalent to the group G itself. We will use the SIP to interpret group theory as the theory of symmetries of mathematical structures in the following section.

3 Higher groups

In this section, we will provide the necessary background for the higher Schreier theorem. We begin by revisiting the theory of higher groups as laid out in [9].

Definition 3.1. A pointed type is type A equipped with a point $a : A$ . We will usually refer to the pointed type by the name of the type A and its basepoint by .

A pointed function is a function $f : A \to B$ that preserves the basepoints . We define the pointed composite by

Definition 3.2. For , its loop space is the type of paths from to itself, pointed at reflexivity:

Loops acts as a functor :

For any pointed type A, the type has a group-like structure given by path composition. If is essentially the only element in A (up to paths), then this group-like structure even determines A in the following way. As we saw in the previous section, the structure identity principle lets us identify the loop space of a type of mathematical structures with with the automorphism group of a canonical example of that structure.

A type is said to be $0$ -connected if there exists a path between any two elements:

Unlike a contractible type where there is a contractible type of paths between any two elements, the path type between elements of a $0$ -connected type may be highly non-trivial. We will exploit these non-trivial path types to give an account of groups as paths in a $0$ -connected type.

Definition 3.3. A type A is $0$ -connected if there is merely a path between any two points of A:

We denote by the type of $0$ -connected types.

Thinking of the type A as a type of mathematical structures, A is $0$ -connected when the theory of that structure is categorical—there is a single model up to (not necessarily unique) isomorphism. As an example, the type of algebraically closures of a field is $0$ -connected; picking a canonical algebraic closure, the loop space of the type of algebraic closures is then, by the structure identity principle, the absolute Galois group of the field.

Lemma 3.4. A pointed function $i : A \to _* B$ between pointed $0$ -connected types is an equivalence if and only if is.

Proof. If f is an equivalence, it is straightforward to show that is an equivalence—this does not require $0$ -connectedness of A and B.

For the converse, we aim to show that the fibers of f are contractible for all $b : B$ on the assumption that is an equivalence. Since being contractible is a proposition and B was assumed $0$ -connected, it will suffice to show that the fiber over the basepoint is contractible.

To show that is contractible, it will therefore suffice to show that for all $a : A$ , , since singleton types are contractible. Note that for any $a : A$ we have a map

Showing that this map is an equivalence is a proposition, and since A is $0$ -connected we may prove this proposition in the case that a is . But in this case, we have a commuting triangle as follows by the definition of :

Since was assumed to be an equivalence, and since composition with a path is an equivalence, we conclude that is an equivalence and therefore that f is as well.

For this reason, pointed connected types are determined by their loop spaces. Following [9], we adopt the perspective that these loop spaces are higher groups, and that the associated pointed connected types are their deloopings.

Definition 3.5. A higher group is a pointed, $0$ -connected type . We refer to as the group itself, while is its “delooping”. A (1-)group is a higher group for which is $1$ -truncated, or equivalently for which is a set.

A homomorphism $\varphi : G \to H$ between higher groups is a pointed function between their deloopings.

Higher groups are concrete groups: they are directly represented as the symmetries of a given object (namely, the base point of their delooping). As we saw above, any This contrasts with abstract groups presented axiomatically as sets equipped with the usual operations.

These two approaches to group theory agree in the case of 1-groups: for any concrete 1-group with delooping , we may define an abstract group structure on using composition of paths. By the functoriality of , a homomorphism induces a homomorphism of abstract groups since any function in Cubical Agda commutes with composition of paths. This functor gives an between the category of concrete 1-groups and the category abstract 1-groups. A formalization of this equivalence is beyond the scope of this paper. We will take for granted that any abstract group G can be delooped by a pointed $0$ -connected type (necessarily $1$ -truncated, since G must be a set), and that homomorphisms between abstract groups are equivalently given by pointed maps between their deloopings. For a full proof of this result, see [2]; see also [20] for a construction of deloopings using higher inductive types.

From now on, we will work only with concrete (higher) groups defined as in Definition 3.5, and will drop the modifier “concrete”. The easiest way to construct examples of higher groups is to take the groups of symmetries of a given element of a type.

Definition 3.6. Let A be a type and $a : A$ an element. Define

to be the type of elements of x which are path connected to a, and define .

It follows quickly by the computation of path in subtypes that and that is $0$ -connected. We will also make the following special definitions in the case that A is a type universe.

Definition 3.7. Let X be a type. We define

and if is a base point, we define

By univalence, is a delooping of the type of self-equivalences . Note that since homomorphisms $G \to H$ between higher groups are pointed maps between their deloopings, deloops the higher group of higher group automorphisms of G. For more examples of concrete deloopings, see [22].

4 The higher Schreier theorem

In this section, we will prove the higher Schreier theorem. First, we must define extensions of higher groups. To do this, we will need the general notion of a fiber sequence.

Definition 4.1. Let A, B, and C be pointed types. A fiber sequence $A \to _* B \to _* C$ consists of a pointed function $f : B \to _* C$ together with a pointed equivalence . The map $A \to _* B$ suggested by the notation $A \to _* B \to _* C$ is defined to be the composite of e with the first projection .

Definition 4.2. Let G and K be higher groups. An extension of G by K consists of a fiber sequence with a $0$ -connected type. We denote the type of extensions by $\mathsf {EXT}(G, K)$ .

Lemma 4.3. In the definition of extension, we do not have to assume that is $0$ -connected:

Proof. Suppose we have with as on the right. Since is $0$ -connected, all fibers of are merely equivalent to the fiber over the base point, which by assumption is equivalent to . Therefore, is equivalent to the sum of $0$ -connected types, indexed by a 0-connected type , and so it itself $0$ -connected.

Our proof of the higher Schreier theorem relies on a general lemma. Recall that for any type A there is an equivalence of type families on A and functions into A given by taking $\Sigma $ -types in one direction and taking fibers in the other [30]. We can extend this equivalence to one for pointed types.

Definition 4.4. Let A be a pointed type. A pointed type family on A is a type family together with a point over the base point of A.

Lemma 4.5. There is an equivalence

between pointed families on A and pointed functions into A.

Proof.

With this lemma in hand, we may derive the higher Schreier theorem.

Theorem 4.6. Let G and K be higher groups. Then

Proof.

The last equivalence follows because is $0$ -connected; since , it follows that for all since by hypothesis.

5 Classifying ordinary extensions

In this section, we will prove that extensions of higher groups defined as in Definition 4.2 generalize extensions of ordinary (1-)groups. We will organize the results in this section in terms of squares of pointed types.

Definition 5.1. A square S of pointed types consists of:

1. 1. Pointed types A, B, C, D;

2. 2. Pointed maps $i : A \to _* B$ , $j : C \to _* B$ , $q : A \to _* C$ and $p : B \to _* D$ ;

3. 3. A path in the type of pointed maps $A \to _* D$ .

Definition 5.2. Given a square of pointed types S, define its loops to be the square

We need a general theorem relating squares of pointed types and their loopings.

Theorem 5.3. Let S be a square of pointed types:

1. 1. If S is a pullback, then so is .

2. 2. If C, q and p are $0$ -connected, then if is a pullback, so is S.

Proof. The first implication may be proven directly. Note that it also implies that for any pointed map $p : B \to _* D$ by taking C to be the unit type.

For the second implication, recall that a square S is a pullback if and only if the induced map is an equivalence for all $c : C$ . If C is $0$ -connected, it suffices to consider , which is a pointed map between pointed types because both q and p are pointed maps and by the commutativity of the square. If q and p are $0$ -connected, then and are both $0$ -connected, and so by Lemma 3.4 it follows that $S_{\ast }$ is an equivalence whenever is. But as a corollary of the first implication, this map is equivalent to . If is a pullback, then is an equivalence, proving the desired implication.

We are now ready to prove the equivalence between extensions as classified in the higher Schreier theorem and the classical notion of extensions between groups. We begin by recalling the classical definition of extension of 1-groups as a short exact sequence.

Definition 5.4. Let G and K be groups. An extension of G by K is a short exact sequence

$$\begin{align*}0 \to K \xrightarrow{i} E \xrightarrow{p} G \to 0 \end{align*}$$

Explicitly, this consists of a group E together with homomorphisms $i : K \to E$ and $p : E \to G$ such that:

1. 1. $p \circ i$ is constant at $1 : G$ ,

2. 2. i is injective,

3. 3. p is surjective,

4. 4. The induced map $K \to \ker (p)$ is an equivalence.

By the definition of groups and group homomorphisms Definition 3.5, the above description of a short exact sequence is by definition equivalent to the following. A short exact sequence is a square of pointed types:

with , , and $0$ -connected such that

1. 1. is injective ( $-1$ -truncated),

2. 2. is surjective ( $-1$ -connected),

3. 3. and is a pullback; equivalently, the induced map $K \to \ker p$ is an equivalence.

To compare the two notions of extension, we begin by putting the definition of extension from Definition 4.2 in a similar form.

Lemma 5.5. Let G and K be higher groups. Extensions of G by K are equivalently pointed pullback squares

Proof. It is generally true that fiber sequences are equivalent to pullback squares of the above sort, since the fiber is the pullback of a point.

We may then put these lemmas together with the help of Theorem 5.3.

Theorem 5.6. Let G and K be groups. Then the type of extensions of G by K is equivalent to the type of short exact sequences $K \to E \to G$ .

Proof. By appealing to Lemma 5.5, it suffices to show that for any square of pointed $0$ -connected types

S is a pullback if and only if is a pullback, is injective, and is surjective. If S is a pullback, then is a pullback by Theorem 5.3; i is injective because has the $0$ -truncated fiber G; p is surjective because has $0$ -connected fiber . Conversely, if p is surjective then is $0$ -connected, and since is also $0$ -connected, Theorem 5.3 again shows that if is a pullback, so is S.

6 Split extensions and semi-direct products

In this section, we will recover the classical classification of split extensions by homomorphic group actions. Recall that deloops the type of pointed automorphisms of , or equivalently higher group automorphisms of K. Therefore, a homomorphic action of G on K—that is, an action of G on K via homomorphisms—is equivalently a pointed map . We will show that such pointed maps classify split extensions.

We begin by defining the holomorph of a higher group K, a classical notion (for 1-groups) which is in a precise sense the universal semi-direct product with K.

Definition 6.1. Consider the function which sends a pointed type merely equivalent to to its underlying type A. By the higher Schreier theorem, this corresponds to an extension:

of by K where

is equivalently the type of doubly pointed types merely equivalent to . This extension is called the holomorph of K.

We will show that an extension is split if and only if its classifying map factors through the map classifying the holomorph of K.

First, we need an abstract lemma related pointed sections to pointed dependent functions.

Definition 6.2. Let be a pointed family of types on A. The type of pointed dependent functions is defined as follows.

If $f : B \to _* A$ is a pointed function, then a pointed section of f is a pointed function $s : A \to _* B$ together with a path in the type of pointed functions $A \to _* A$ .

Lemma 6.3. Let A be a pointed type. The equivalence of Lemma 4.5 between pointed families on A and pointed functions into A extends to an equivalence between pointed dependent functions of a pointed family on A and pointed sections of a pointed function into A.

Now we define split exact sequences of higher groups and prove our desired classification.

Definition 6.4. Let be an extension of higher groups. A splitting of this extension is a pointed map together with a path in the type of pointed maps .

A split extension is an extension with a choice of splitting.

Theorem 6.5. Let be an extension of higher groups classified by a map . Then splittings of this extension correspond to pointed factorizations of c through .

Proof. We may consider c to be a pointed family by transporting over . By Lemma 6.3, splittings of the extension are therefore equivalent to pointed dependent functions . It remains to show that

We compute as follows: