Classification of short exact sequences

Short exact sequences A → E → B of abelian groups are classified by pointed maps K(B,n.+2) ->* K(A,n.+3), for any n : nat. This is Christensen and Flaten, "Ext groups in homotopy type theory", Theorem 2.2.2, and the following comment. Here we prove it for general n from the start.

Applying (K-, n.+1) to a short exact sequence of an abelian groups gives a fiber sequence

The identifications equiv_g_pi_n_em carry Pi n.+1 of the sequence K(-, n.+1) applied to E back to E itself, so that sequence is exact.

K(-, n.+1) sends short exact sequences of abelian groups to fiber sequences of Eilenberg-Mac Lane spaces. The hypotheses of isexact_purely_isexact_pi are found by typeclass search: the spaces are n-connected and n.+1-truncated, fmap (K' n.+1) of the projection is n-connected since the projection is surjective, and fmap (K' n.+1) of the inclusion is an embedding on Pi n.+1 since the inclusion is an embedding.

The classifying map of a short exact sequence

We associate to each short exact sequence A → E → B the connecting map of the fiber sequence K(A,n.+3) → K(E,n.+3) → K(B,n.+3), expressed as a pointed map K(B,n.+2) ->* K(A,n.+3).

The short exact sequence of a pointed map

Conversely, a pointed map f : K(B,n.+2) ->* K(A,n.+3) yields a short exact sequence A → Pi n.+2 (pfiber f) → B, by rotating the fiber sequence of f and taking homotopy groups.

The inclusion of the short exact sequence is given by the composite of the identification of A with Pi n.+2 (loops K(A, n.+3)) and Pi n.+2 applied to the connecting map loops K(A,n+3) → pfiber f of the fiber sequence.

The projection is similarly induced by the fiber inclusion of f.

The two homotopy groups neighbouring the sequence vanish: Pi n.+2 K(A, n.+3) lies below the connectivity of K(A, n.+3), and Pi n.+3 K(B, n.+2) lies above the truncation level of K(B, n.+2).

The three conditions defining a short exact sequence therefore come from the long exact sequences of the fiber sequence of f and of its rotation.

The short exact sequence associated to f.

abses_pfiber composed with abses_classifying_map is the identity

In other words, the short exact sequence extracted from the classifying map of E is E itself.

This square arises three times below, so we state it as a local result. The RHS is just the definition abses_classifying_map, so the only difference is the postcomposition of the pointed identity map.

The fiber of the classifying map is loops K(E,n.+3). Precomposing with the loop identification of K(B,n.+2) does not change the fiber, so it is the fiber of the connecting map, which pequiv_pfiber_connecting_map identifies with loops K(E,n.+3).

Through this identification, the fiber inclusion of the classifying map is loops of the projection.

Through the same identification, the connecting map of the fiber sequence of the classifying map is loops of the inclusion.

The middle isomorphism of the round trip.

It commutes with the inclusions.

It commutes with the projections.

The short exact sequence extracted from the classifying map of E is E.

The classifying map of the sequence of a delooped map

Rather than proving that the other composite is the identity, we will define an a priori different section of abses_classifying_map. To do this, we first show that for psi : K(B,n.+3) ->* K(A,n.+4), the classifying map K(B,n.+2) ->* K(A,n.+3) of abses_pfiber psi is fmap loops psi (with corrected endpoints) precomposed with negation on K(B,n.+2). Since every map K(B,n.+2) ->* K(A,n.+3) can be delooped to such a psi, this will give a section of abses_classifying_map in abses_classifying_section below.

The fiber of a map from an n.+2-connected type to an n.+3-connected type is n.+2-connected.

The fiber of psi is the Eilenberg-Mac Lane space of its homotopy group in degree n.+3, by pequiv_em_connected_truncated. On Pi n.+3, that identification is the inverse of equiv_g_pi_n_em.

Through that identification, fmap (K' n.+3) of the projection is the fiber inclusion of psi.

Through that identification, fmap (K' n.+3) of the inclusion is the connecting map of psi, modulo the loop identification of K(A,n.+3).

The projection triangle enlarged to a square.

The two squares above form a map from the fiber sequence of Eilenberg-Mac Lane spaces of the extracted sequence to the fiber sequence of pfib psi in the sense required by connecting_map_natural_isexact.

Through the loop identification of K(A,n.+3), the connecting map of the extracted fiber sequence is loops psi, twisted by loop inversion.

Negation on K(B,n.+2), as loop inversion conjugated by the loop identification. It should agree with fmap (K' n.+2) ab_homo_negation, since both act by inversion on Pi n.+2, but we do not need that here.

Under the loop identification, pequiv_neg_em is loop inversion.

The classifying map of the extracted sequence is equiv_loops_em_pmap applied to psi, twisted by pequiv_neg_em. Recall that equiv_loops_em_pmap is fmap loops conjugated by the loop identifications.

The classification theorem

abses_classifying_map is an equivalence, with inverse abses_pfiber.

We declare u so that it refers to the same universe in the Context and in equiv_ext_classifying.

A section of the classifying map.

The map abses_classifying_map has a retraction abses_pfiber by abses_pfiber_abses_classifying_map and a section by abses_classifying_section. Therefore it is an equivalence. This proof uses abses_pfiber as the inverse.

Short exact sequences A → E → B are classified by pointed maps K(B,n.+2) ->* K(A,n.+3).

Consequently Ext B A is the set of path components of the classifying mapping type. Since Trunc is cumulative, we can take the truncation in the universe u of B and A, rather than in the larger universe of Ext B A.

Smallness

AbSES B A is essentially small, and so is Ext B A. We use the case n = 0 of the classification.

Naturality of the classifying map

A morphism of short exact sequences induces a commuting square relating the two classifying maps.

K(-,n.+3) of the projection square of phi.

K(-,n.+3) of the inclusion square of phi.

The two squares above form a map between the fiber sequences of Eilenberg-Mac Lane spaces.

A morphism of short exact sequences induces a commuting square of classifying maps, by naturality of the connecting map and of the loop identification.