Formalising Yoneda Ext in Univalent Foundations

TL;DR

This paper formalises Yoneda Ext groups within homotopy type theory using Coq-HoTT, avoiding resolutions and providing new formal proofs of classical exact sequences and properties.

Contribution

It introduces a resolution-free formalisation of Ext groups in HoTT, with novel proofs of exact sequences and implementation of Ext as a bifunctor.

Findings

Formalisation of Ext groups in HoTT without resolutions

Proof of the six-term exact sequence via fibre sequences

Implementation of Ext as a bifunctor

Abstract

Ext groups are fundamental objects from homological algebra which underlie important computations in homotopy theory. We formalise the theory of Yoneda Ext groups in homotopy type theory (HoTT) using the Coq-HoTT library. This is an approach to Ext which does not require projective or injective resolutions, though it produces large abelian groups. Using univalence, we show how these Ext groups can be naturally represented in HoTT. We give a novel proof and formalisation of the usual six-term exact sequence via a fibre sequence of 1-types (or groupoids), along with an application. In addition, we discuss our formalisation of the contravariant long exact sequence of Ext, an important computational tool. Along the way we implement and explain the Baer sum of extensions and how Ext is a bifunctor.

Equations

$${\text{Ext}}^1(Z/n,A)\cong A/n$$

$$\cdots \stackrel{i^{\ast }}{\to }{\text{Ext}}^n(A,G)\stackrel{-⊚E}{\to }{\text{Ext}}^{n+1}(B,G)\stackrel{p^{\ast }}{\to }{\text{Ext}}^{n+1}(E,G)\stackrel{i^{\ast }}{\to }\cdots to0.0pt.\text{hss}$$

$$\text{idtoequiv}:\prod _{X,Y:\mathrm{Type}}(X=Y)\to (X\simeq Y)$$

$$\text{prod@{u} X Y }\equiv \text{ prod@{v} X Y}.$$

$$\big{(}\lvert E\lvert_{0}=_{\operatorname{Ext}^{1}}\lvert F\lvert_{0}\big{)}\ \simeq\ \lVert E=F\lVert$$

$$(E{=}_{\mathrm{AbSES}(B,A)}F)\simeq \text{abses\_path\_data\_iso}(E,F).$$

$$(E=F)\simeq \text{abses\_path\_data\_iso}(E,F)\simeq \text{abses\_path\_data}(E,F).$$

$$B\to A\oplus B\stackrel{\varphi }{\to }A\oplus B\to A.$$

$${\mathrm{Ext}}^1(f,-)\circ {\mathrm{Ext}}^1(-,g)={\mathrm{Ext}}^1(-,g)\circ {\mathrm{Ext}}^1(f,-).$$

$$A$$

$$E+F:\equiv {\Delta }^{\ast }{\nabla }_{\ast }(E\oplus F)$$

$${\alpha }_{\ast }(E+F)$$

$$={\Delta }^{\ast }({\nabla }_{\ast }({\alpha }_{\ast }E\oplus {\alpha }_{\ast }F))\equiv {\alpha }_{\ast }E+{\alpha }_{\ast }F.$$

$$\cdots \to {\pi }_n(F)\to {\pi }_n(E)\to {\pi }_n(B)\to \cdots \to {\pi }_0(F)\to {\pi }_0(E)\to {\pi }_0(B).$$

$$i^{\ast }(F)$$

$$i^{\ast }{p}^{\ast }(F/A)$$

$$\Omega \mathrm{AbSES}(B,A)$$

$$B^{\prime }$$

$$0$$

$${\mathrm{Ext}}^1(Z/n,A)\cong A/n.$$

$$\cdots \to \mathrm{Hom}(Z,A)\stackrel{n^{\ast }}{\to }\mathrm{Hom}(Z,A)\to {\mathrm{Ext}}^1(Z/n,A)\to {\mathrm{Ext}}^1(Z,A)\to \cdots$$

$$F⊚E:\equiv (F,E{)}_B:{\mathrm{ES}}^n(B,A)\to \mathrm{AbSES}(C,B)\to {\mathrm{ES}}^{n+1}(C,A).$$

$$\cdots \stackrel{i^{\ast }}{\to }{\text{Ext}}^n(A,G)\stackrel{-⊚E}{\to }{\text{Ext}}^{n+1}(B,G)\stackrel{p^{\ast }}{\to }{\text{Ext}}^{n+1}(E,G)\stackrel{i^{\ast }}{\to }\cdots to0.0pt.\text{hss}$$

$$(A\stackrel{l}{\to }Y\stackrel{s}{\to }{B}^{\prime },B^{\prime }\stackrel{k}{\to }X\stackrel{r}{\to }C),(A\stackrel{j}{\to }F\stackrel{q}{\to }B,B\stackrel{i}{\to }E\stackrel{p}{\to }C).$$

$$A$$

Full text

Formalising Yoneda Ext in Univalent Foundations

Jarl G. Taxerås Flaten

1 Introduction

The field of homotopy type theory (HoTT) lies at the intersection of type theory and algebraic topology, and serves as a bridge to transfer tools and insights from one domain to the other. In one direction, the formalism of type theory has proven to be a powerful language for reasoning about some of the highly coherent structures occurring in branches of modern algebraic topology. Several of these structures are “natively supported” by HoTT, and we can reason about them much more directly than in classical set-based approaches. This makes HoTT an ideal language in which to formalise results and structures from algebraic topology. Moreover, theorems in HoTT are valid in any $\infty$-topos, not just for ordinary spaces. Details about the interpretation of our constructions into an $\infty$-topos, and the relation of our Ext groups to sheaf Ext, are discussed in [2].

We present a formalisation of Ext groups in HoTT following the approach of Yoneda [12, 13]. Ext groups are fundamental objects in homological algebra, and they permeate computations in homotopy theory. For example, the universal coefficient theorem relates Ext groups and cohomology, and features in the classical proof that $\pi_{5}(S^{3})\simeq\operatorname{\mathbb{Z}}/2$. Much of our formalisation has already been accepted into the Coq-HoTT library under the Algebra.AbSES namespace, though we have also contributed to other parts of the library throughout this project. The long exact sequence, along with a few other results we need, are currently in a separate repository named Yoneda-Ext. We supply links to formalised statements using a trailing ♢-sign throughout.

In ordinary mathematics, Ext groups of modules over a ring are usually defined using projective (or injective) resolutions. This is possible because the axiom of choice implies the existence of such projective resolutions, and Ext groups are independent of any particular choice of resolution. (Similarly, categories of sheaves of modules always admit injective resolutions.) In our setting, however, even abelian groups fail to admit projective resolutions. This stems from the fact that some sets fail to be projective, which may be familiar to those working constructively or internally to a topos. Accordingly, to define Ext groups in homotopy type theory we cannot rely on resolutions. Fortunately, Yoneda [12, 13] gave such a general approach, whose theory is detailed in [6], our main reference. A drawback of this approach is that it produces large abelian groups, as we explain in Section 3.1.

We build upon the Coq-HoTT library [3], which contains sophisticated homotopy-theoretic results, but which is presently lacking in terms of “basic” algebra. For this reason, we have opted to simply develop Ext groups of abelian groups, instead of for modules over a ring or in a more general setup. Nevertheless, it is clear that everything we do could have been done over an arbitrary ring, given a well-developed library of module theory. Moreover, we emphasise that higher Ext groups in HoTT are interesting even for abelian groups. While in classical mathematics such Ext groups of abelian groups are trivial in dimension $2$ and up, in HoTT they may be nontrivial in all dimensions! This is because there are models of HoTT in which these Ext groups are nontrivial [2].

In Section 3 we explain how univalence lets us naturally represent Yoneda’s approach to Ext in HoTT. We construct the type $\operatorname{{\verb~AbSES~}}(B,A)$ of short exact sequences between two abelian groups $A$ and $B$, and define $\operatorname{{\verb~Ext~}}^{1}(B,A)$ to be the set of path-components of $\operatorname{{\verb~AbSES~}}(B,A)$. This definition is justified by characterising the paths in $\verb+AbSES+(B,A)$, which crucially uses univalence. We also show that the loop space of $\verb+AbSES+(B,A)$ is isomorphic to the group $\verb+Hom+(B,A)$ of group homomorphisms, and that $\verb+Ext+^{1}(P,A)$ vanishes whenever $P$ is projective, in a sense we define. These results all play a role in the subsequent sections.

The main content of Section 4 is a proof and formalisation of the following:

Theorem 4.1**.**

Let $A\xrightarrow{i}E\xrightarrow{p}B$ be a short exact sequence of abelian groups. For any abelian group $G$, pullback yields a fibre sequence: $\operatorname{{\verb~AbSES~}}(B,G)\xrightarrow{p^{*}}\operatorname{{\verb~AbSES~}}(E,G)\xrightarrow{i^{*}}\operatorname{{\verb~AbSES~}}(A,G).$♢

We give a novel, direct proof of this result which requires managing considerable amounts of coherence. The formalisation is done for abelian groups, but the proof applies to modules over a general ring. Its formalisation benefited from the WildCat library of Coq-HoTT (see Section 2.2), which makes it convenient to work with types equipped with an imposed notion of paths. This allows us to work with path data in $\operatorname{{\verb~AbSES~}}(B,A)$ with better computational properties than actual paths, but which correspond to paths via the aforementioned characterisation. From the fibre sequence of the theorem we deduce the usual six-term exact sequence (Proposition 4.11), which we then use to compute Ext groups of cyclic groups:

[TABLE]

for any nonzero $n:\operatorname{\mathbb{N}}$ and abelian group $A$ (Corollary 4.14).♢ The six-term exact sequence, along with this corollary, have already been applied in [1]. We also discuss how $\operatorname{{\verb~Ext~}}^{1}$ becomes a bifunctor into abelian groups using the Baer sum.

Finally, in Section 5 we define $\verb+Ext+^{n}$ for any $n:\operatorname{\mathbb{N}}$ and discuss our formalisation of the long exact sequence, in which the connecting maps are given by splicing:♢

Theorem 5.5**.**

Let $A\xrightarrow{i}E\xrightarrow{p}B$ be a short exact sequence of abelian groups. For any abelian group $G$, there is a long exact sequence by pulling back:\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/LES.v#L15\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/LES.v#L47\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/LES.v#L94

[TABLE]

At present, we have only formalised this long exact sequence of pointed sets. It remains to construct the Baer sum making $\operatorname{{\verb~Ext~}}^{n}$ into an abelian group for $n>1$, however once this is done then we automatically get a long exact sequence of abelian groups. Our proof follows that of Theorem 5.1 in [6], which is originally due to Stephen Schanuel.

Notation and conventions

We use typewriter font for concepts which are defined in the code, such as AbSES and Ext. In contrast, when we use normal mathematical font, such as $\operatorname{Ext}^{n}(B,A)$, we mean the classical notion. For mathematical statements we prefer to stay close to mathematical notation by writing for example $\verb+Ext+^{n}(B,A)$ for what means $\verb+Ext n B A+$ in Coq. The symbol ♢ is used to refer to relevant parts of the code.

Our terminology mirrors that of [10]; in particular we say ‘path types’ for what are also called ‘identity types’ or ‘equality types’. We write $\operatorname{{\verb~pType~}}$ for the universe of pointed types, and $\operatorname{\verb~pt~}$ for the base point of a pointed type. The $\equiv$-symbol is for definitional equality.

2 Preliminaries

2.1 Homotopy Type Theory

We briefly explain the formal setup of homotopy type theory along with some basic notions that we need. For a thorough introduction to HoTT, the reader may consult [10, 9].

Homotopy type theory (HoTT) extends Martin–Löf type theory (MLTT) with the univalence axiom and often various higher inductive types (HITs). Of the latter, we simply need propositional truncation and set truncation, which we explain in more detail below.

The univalence axiom characterises the identity types of universes. In ordinary MLTT, there is always a function

[TABLE]

defined by sending the reflexivity path on a type $X$ to the identity self-equivalence on $X$, using the induction principle of path types. The univalence axiom asserts that idtoequiv is an equivalence for all $X$ and $Y$. In HoTT, the first thing we often do after defining a new type is to characterise its path types. The univalence axiom does this for the universe.

From univalence, a general structure identity principle [10, Chapter 9.8] follows which characterises paths between structured types, such as groups and other algebraic structures. In the case of groups, univalence implies that paths between groups correspond to group isomorphisms. Similarly, paths between modules correspond to module isomorphisms.

Propositions, sets, and groupoids

In HoTT there is a hierarchy of $n$-truncated types (or $n$-types, for short) for any integer $n\geq-2$. In general, a type $X$ is an $(n+1)$-type when all the path types $x_{0}=_{X}x_{1}$ are $n$-types. The recursion starts at $-2$, when the condition is just that the map $X\to 1$ is an equivalence, and in this case $X$ is contractible.

We only deal with the bottom four levels of this hierarchy: contractible types, propositions ($(-1)$-types), sets (0-types) and 1-types. A type $X$ is a proposition when any two points in $X$ are equal (but there may not be any points). A type $X$ is a set when the path types $x_{0}=_{X}x_{1}$ are all propositions—this amounts to there being “at most” one path between $x_{0}$ and $x_{1}$. Lastly, a type $X$ is a 1-type when its path types are sets—in particular, for any $x:X$, the loop space $\Omega X:\equiv(x=_{X}x)$ is a set which is a group under path composition. (We leave base points implicit when taking loop spaces.)

There are truncation operations which create a proposition or a set from a given type $X$. We denote by $\lVert X\lVert$ the propositional truncation, and by $\pi_{0}{X}$ the set truncation (or set of path-components) of $X$. In Coq-HoTT, the corresponding notation is merely X and Tr 0 X. The map $\verb~tr~:X\to\pi_{0}X$ sends a point to its connected component. When we say that a type $X$ merely holds, then we mean that its propositional truncation $\lVert X\lVert$ holds.

2.2 The Coq-HoTT Library

The Coq-HoTT library [3] is an open-source repository of formalised mathematics in homotopy type theory using Coq. It is particularly aimed at developing synthetic homotopy theory, and includes theory about spheres, loop spaces, classifying spaces, modalities, “wild $\infty$-categories,” and basic results about abelian groups, to mention a few things. The library is part of the Coq Platform and is available through the standard opam package repositories.

Below we explain some of the main features of this library, and of Coq itself, which are important for the present work.

Universes and cumulativity

We assume basic familiarity with universes and universe levels in Coq, and in particular that they are cumulative: a type $X:\verb+Type@{u}+$ can be resized to live in Type@{v} under the constraint $\verb+u+\leq\verb+v+$. (Here u and v are universe levels.) Resizing is done implicitly by Coq.

In the Coq-HoTT library, we additionally make most of our structures cumulative. This essentially means that resizing commutes with the formation of a data structure—i.e., it does not matter whether you resize the inputs to the data structure or whether you resize the resulting data structure. As an example, consider the data structure prod which forms the product of two types in a common (for simplicity) universe level. Suppose we have two universe levels u and v with the constraint u < v. Given X Y : Type@{u}, we can form the product at level u and then resize, or first resize and then form the product. By making prod a cumulative data structure, the two results agree (with implicit resizing):

[TABLE]

Cumulativity of data structures is an essential Coq feature which facilitates the kind of formalisation we do in this paper. For example, it lets us resize groups and homomorphisms. It also lets us reduce the number of universes in some of our definitions via the following trick: instead of having separate universes for different inputs, we can often use a single universe (which represents the maximum) and leverage cumulativity.

We also make use of universe constraints since our constructions move between various universe levels. The constraints both document and verify the mathematical intent.

The WildCat library

The WildCat namespace contains the development of “wild $\infty$-categories,” functors between such, and related things. This library was spearheaded by Ali Caglayan, tslil clingman, Floris van Doorn, Morgan Opie, Mike Shulman, and Emily Riehl. The concepts generalise those appearing in [11, Section 4.3.1], and are not currently present in the literature. We explain the basics of this library which are especially relevant for our formalisation.

Starting from the notion of graph♢—a type $A$ with a binary operation (or correspondence) $\operatorname{{\verb~Hom~}}$ into $\operatorname{\verb~Type~}$—the notion of a 0-functor♢ is that of a homomorphism of graphs:

⬇

Class IsGraph (A : Type) := { Hom : A -> A -> Type }.

Class Is0Functor {A B : Type} ‘{IsGraph A} ‘{IsGraph B} (F : A -> B)

:= { fmap : forall {a b : A} (f : Hom a b), Hom (F a) (F b) }.

We will often use the notation $\operatorname{{\verb~Hom~}}$ in this text, leaving the graph structure implicit.

From here one could go ahead and define categories by defining a composition operation and using the identity types of the type $\operatorname{{\verb~Hom~}}(a,b)$ to express the various laws a category needs to satisfy, such as associativity of composition. A more flexible approach is to instead allow $\operatorname{{\verb~Hom~}}(a,b)$ to itself be a graph, making $A$ into a 2-graph.♢ This is the approach taken by WildCat, and this flexibility is important for our formalisation.

⬇

Class Is2Graph (A : Type) ‘{IsGraph A}

:= { isgraph_hom : forall (a b : A), IsGraph (Hom a b) }.

For a $2$-graph $A$, a category structure can then be defined in a straightforward manner using isgraph_hom to express the various laws that need to hold. This structure is bundled into a class called Is1Cat.♢ For example, associativity is expressed as follows, using the notation $== as a shorthand for the$2$-graph structure and$o for composition:

⬇

cat_assoc : forall (a b c d : A)

(f : Hom a b) (g : Hom b c) (h : Hom c d),

  (h $o g) $o f $== h $o (g $o f);

If all the morphisms in $A$ are invertible, then $A$ is a groupoid.♢ Finally, for the notion of a $1$-functor between categories we also express the laws using the $2$-graph structure.♢

⬇

Class Is1Functor {A B : Type} ‘{Is1Cat A} ‘{Is1Cat B}

(F : A -> B) ‘{!Is0Functor F} := {

fmap_id : forall a, fmap F (Id a) $== Id (F a);

fmap_comp : forall a b c (f : Hom a b) (g : Hom b c),

  fmap F (g $o f) $== fmap F g $o fmap F f;

fmap2 : forall a b (f g : Hom a b),

  (f $== g) -> (fmap F f $== fmap F g) }.

The terms fmap_id and fmap_comp express that the functor F respects identities and composition, as usual. If we had used identity types instead of a $2$-graph structure, so that f $== g simply meant f = g, then F would automatically respect equality between morphisms, making fmap2 redundant. However, in the more general$2$-graph setup, this needs to be included as a law.

The adjective “wild” is used for the sort of categories just defined to indicate that they do not capture all the coherence needed to represent $\infty$-categories, only the $1$-categorical structure. However, in our usage we will only encounter genuine $1$-categories and groupoids. In particular, any type $X$ defines a groupoid via its identity types♢, and if $X$ is a $1$-type then this groupoid structure captures everything about $X$. This enables us to impose our own notion of paths, which we call path data below, for certain types of interest.

3 Yoneda Ext

As mentioned in the introduction, we will follow Yoneda’s approach to Ext groups [12, 13], which does not require projective (or injective) resolutions, though it produces large groups. This approach and related theory is explained in [6], which is our main reference. At present, the Coq-HoTT library—with which this work has been formalised—does not contain much theory related to modules over a general ring (nor the theory of abelian categories, or anything of the sort). We therefore only formalise and state our results for abelian groups. It is clear, however, that everything we say could be done for modules over a general ring.

For the classically-minded reader, let us also emphasise that in homotopy type theory the category of abelian groups does not have global dimension $1$, so that the higher Ext groups we define in Section 5 do not necessarily vanish.

3.1 The Type of Short Exact Sequences

Given two abelian groups $A$ and $B$, Yoneda defines a group $\operatorname{Ext}^{1}(B,A)$ by considering the large set (or class) of all short exact sequences $A\xrightarrow{i}E\xrightarrow{p}B$ and taking a quotient by a certain equivalence relation. The sequence being exact means that $i$ is injective, $p$ is surjective, that $p\circ i=0$, and that the image of $i$ is equal to the kernel of $p$. We usually simply write $E$ for the short exact sequence $A\to E\to B$ when no confusion can arise. The equivalence relation which Yoneda quotients out by is defined as “$E\sim F$ if and only if there exists an isomorphism $E\cong F$ which respects the maps from $A$ and to $B$.” Equivalently, but more topologically, one can consider the groupoid of short exact sequences $A\to E\to B$ and define $\operatorname{Ext}^{1}(B,A)$ to be the set of path-components of this groupoid—see, e.g., [6, Chapter III] for details about both of these descriptions.

In homotopy type theory, given two abelian groups $A$ and $B$ we form the type of short exact sequences from $A$ to $B$ as the $\Sigma$-type over all abelian groups $E$ equipped with an injection $\mathtt{inclusion}_{E}:A\to E$, a surjection ${\verb+projection+}_{E}:E\to B$, and a witness that these two maps form an exact complex. We represent this data as the following record-type:♢

⬇

Record AbSES@{u v | u < v} (B A : AbGroup@{u}) : Type@{v} := {

middle : AbGroup@{u};

inclusion : Hom A middle;

projection : Hom middle B;

isembedding_inclusion : IsEmbedding inclusion;

issurjection_projection : IsSurjection projection;

isexact_inclusion_projection

  : IsExact (Tr (-1)) inclusion projection;

}.

Note that $\operatorname{{\verb~AbSES~}}(B,A)$ denotes short exact sequences from $A$ to $B$. The abelian group middle plays the role of $E$ in the prose above. Here, the condition that $\verb+projection+_{E}\circ\verb+inclusion+_{E}=0$ is baked into the IsExact field, which also expresses exactness.111The term Tr (-1) can safely be ignored; it expresses that the induced map from $A$ to the kernel of $\verb~projection~_{E}$ is $(-1)$-connected, which here just means it is a surjection. We have included universe annotations which express that $E$ lives in the same universe u as the abelian groups $A$ and $B$. Accordingly, the resulting type AbSES$(B,A)$ lives in a universe v which is strictly greater than u, as in Yoneda’s construction above. The type AbSES$(B,A)$ is pointed by the trivial short exact sequence♢ $A\to A\oplus B\to B.$

We now define $\operatorname{{\verb~Ext~}}^{1}(B,A)$ as the set-truncation of the type of short exact sequences.♢

⬇

Definition Ext (B A : AbGroup) := Tr 0 (AbSES B A).

In Section 3.3 we make the set $\operatorname{{\verb~Ext~}}^{1}(B,A)$ into an abelian group via the Baer sum. These abelian groups, and their higher variants defined in Section 5, are our main objects of study.

Whenever we define a new type in homotopy type theory, the first thing we often do is to characterise its path types. Theorem 7.3.12 of [10] characterises paths in truncations, yielding

[TABLE]

for any $E,F:\operatorname{{\verb~AbSES~}}(B,A)$. As such, it suffices to understand paths in AbSES$(B,A)$. These are in turn characterised by Theorem 2.7.2 of loc. cit., which characterises paths in general $\Sigma$-types, combined with the fact that paths in AbGroup are isomorphisms. In our case, the result is that paths between short exact sequences correspond to isomorphisms between the middles making the appropriate triangles commute. We refer to this data as path data, and bundle it into a separate type (where * denotes products of types):♢

⬇

Definition abses_path_data_iso {B A : AbGroup} (E F : AbSES B A)

:= {phi : Iso E F & (phi $o inclusion E == inclusion F)

                  * (projection E == projection F $o phi)}.

Here Iso forms the type of isomorphisms between two groups. From our discussion above, for any $E,F:\operatorname{{\verb~AbSES~}}(B,A)$, we get an equivalence of types♢

[TABLE]

However, a bit more can be said: the short five lemma♢ implies that if we replace Iso by Hom above, then it still follows that phi is an isomorphism. We define abses_path_data♢ as abses_path_data_iso above, but with Hom in place of Iso. It is convenient to have both types around: it is easier to construct an element of abses_path_data; however we will see situations later on where it is convenient to keep track of a specific inverse to the underlying map, which abses_path_data_iso lets us do.

Definition 3.1**.**

The type $\operatorname{{\verb~AbSES~}}(B,A)$ is a groupoid whose graph structure is given by abses_path_data_iso and a corresponding category structure. For the $2$-graph structure, we assert that two path data are equal just when their underlying maps are homotopic.♢

This definition is justified by the preceding discussion, which yields:

Lemma 3.2**.**

For any $E,F:{\verb+AbSES+}(B,A)$, there are equivalences of types♢

[TABLE]

Though elementary, this lemma has an interesting consequence. This statement appears as the $n,i=1$ case of [8, Theorem 1].

Proposition 3.3**.**

The loop space of $\verb+AbSES+(B,A)$ is naturally isomorphic to $\operatorname{{\verb~Hom~}}(B,A)$.♢

Proof 3.4**.**

It suffices, by the previous lemma, to give an isomorphism between $\operatorname{{\verb~Hom~}}(B,A)$ and $\verb+abses_path_data+(A\oplus B,A\oplus B)$. One can easily check that a map $\phi:A\oplus B\to A\oplus B$ subject to the constraints of path data, is uniquely determined by the composite♢

[TABLE]

Moreover, this association defines a group isomorphism—details are in the formalisation.♢

To formalise the previous proposition, we first developed basic theory about biproducts of abelian groups which now live in Algebra.AbGroups.Biproduct.

In ordinary homological algebra, an abelian group $P$ is projective if for any homomorphism $f:P\to B$ and epimorphism $p:A\to B$, there exists a lift $l:P\to A$ such that $f=e\circ l$. It is well-known that $\operatorname{Ext}^{1}(P,A)$ always vanishes when $P$ is projective, and that this property characterises projectivity. In our setting, we define an abelian group $P$ to be projective if for any homomorphism $f$ and epimorphism $p$ as above, there merely exists a lift $l$ such that $f=l\circ l$. The propositional truncation makes this into a property of an abelian group, and not a structure. In Coq, we express this as a type-class:♢

⬇

Class IsAbProjective (P : AbGroup) : Type :=

isabprojective : forall (A B : AbGroup),

forall (f : Hom P B), forall (e : Hom A B),

IsSurjection e -> merely (exists l : P $-> A, f == e $o l).

As in the classical case, projectives are characterised by the vanishing of Ext:

Proposition 3.5**.**

An abelian group $P$ is projective if and only if $\operatorname{{\verb~Ext~}}^{1}(P,A)=0$ for all $A$.♢

From the induction principle of $\operatorname{\mathbb{Z}}$ it follows that $\operatorname{\mathbb{Z}}$ is projective♢ in the sense we defined above. Consequently $\operatorname{{\verb~Ext~}}^{1}(\operatorname{\mathbb{Z}},A)=0$ for any abelian group $A$, and we will use this later on.

Remark 3.6**.**

There is a subtle point related to projectivity that merits discussion. Our definition of projectivity only requires the lift $l$ to merely exist (a property), but one could have asked for actual existence (a structure). There is no concept of “mere existence” in ordinary mathematics, and when translating concepts into HoTT we have to carefully choose to make something a structure or a property. In this case, our definition of projectivity is justified by Proposition 3.5. If we had made projectivity a structure, then not even $\operatorname{\mathbb{Z}}$ would be projective, which we need it to be.

3.2 Ext as a Bifunctor

Some of the important structure of $\operatorname{Ext}^{1}$ is captured by the fact that it defines a bifunctor $\operatorname{Ext}^{1}(-,-):\operatorname{Ab}^{\operatorname{op}}\times\operatorname{Ab}\to\operatorname{Ab}.$ This means that $\operatorname{Ext}^{1}(-,-)$ is a functor in each variable and that the following “bifunctor law” holds:

[TABLE]

We added a basic implementation of bifunctors to the WildCat library for our purposes, asserting the bifunctor law using the $2$-graph structure:♢

⬇

Class IsBifunctor {A B C : Type} ‘{IsGraph A, IsGraph B, Is1Cat C}

(F : A -> B -> C) := {

bifunctor_isfunctor_10 : forall a, Is0Functor (F a);

bifunctor_isfunctor_01 : forall b, Is0Functor (fun a => F a b);

bifunctor_isbifunctor :

  forall a0 a1 (f : Hom a0 a1), forall b0 b1 (g : Hom b0 b1),

    fmap (F _) g $o fmap (flip F _) f

      $== fmap (flip F _) f $o fmap (F _) g }.

Here flip is the map which reverses the order of arguments of a binary function. We note that in order to state the bifunctor law, we only require F to be a [math]-functor in each variable. As such we only include those instances in this class.

The bifunctor instance of $\operatorname{{\verb~Ext~}}^{1}$ will come from a bifunctor instance of $\operatorname{{\verb~AbSES~}}$, so we work with the latter. First of all, $\operatorname{{\verb~AbSES~}}:\verb~AbGroup~^{\operatorname{op}}\to\verb~AbGroup~\to\verb~Type~$ becomes a [math]-functor in each variable by pulling back and pushing out, respectively.

Lemma 3.7**.**

Let $g:B^{\prime}\to B$ be a homomorphism of abelian groups. For any short exact sequence $A\to E\to B$, we have a short exact sequence $A\to g^{*}(E)\to B^{\prime}$.♢ Moreover, if $E$ is trivial, then so is the short exact sequence $g^{*}(E)$.♢

Dually, one can push out a short exact sequence $A\to E\to B$ along a map $f:A\to A^{\prime}$ to get a short exact sequence $A^{\prime}\to f_{*}(A)\to B$.♢

We supply careful proofs that pushout and pullback respect composition of pointed maps♢ and homotopies between maps,♢ and that pushing out along the identity map gives the pointed identity map.♢ These identities could be shown with shorter proofs, however in Section 4 we will have to prove coherences involving the paths constructed here, and these coherences are simpler to solve when phrased in terms of path data. In any case, these proofs make $\operatorname{{\verb~AbSES~}}$ into a $1$-functor in each variable.♢♢

For the bifunctor law we make use of the following proposition, which is remarkably useful for showing that a given extension is a pullback of another one.

Proposition 3.8**.**

Suppose given the following diagram with short exact rows:

[TABLE]

If $\alpha=\operatorname{id}$ then the top row is equal to the pullback of the bottom row along $g$.♢

Proof 3.9**.**

Since the right square commutes, we get a map $E^{\prime}\to g^{*}(E)$ by the universal property of the pullback. This map respects the inclusions and projections, and therefore defines a path by Lemma 3.2.

There is a dual statement for pushouts in which the rightmost map must be the identity.♢

Corollary 3.10**.**

Any diagram with short exact rows as follows yields a path $f_{*}(E)=g^{*}(F)$.♢

[TABLE]

The corollary lets us swiftly show bifunctoriality:

Proposition 3.11**.**

The binary map $\operatorname{{\verb~AbSES~}}:\verb~AbGroup~^{\operatorname{op}}\to\verb~AbGroup~\to\operatorname{\verb~Type~}$ is a bifunctor.♢

Proof 3.12**.**

Consider a short exact sequence $A\to E\to B$ along with two homomorphisms $f:A\to A^{\prime}$ and $g:B^{\prime}\to B$. There is an obvious diagram with short exact rows:

[TABLE]

which by the previous corollary yields a path $f_{*}(g^{*}(E))=g^{*}(f_{*}(E))$, as required.

Remark 3.13**.**

The results from Section 3.3 will show that $\operatorname{{\verb~AbSES~}}$ is an $H$-space.♢ Combining this with [1, Lemma 2.6]♢, we deduce that $\operatorname{{\verb~AbSES~}}$ is a bifunctor into pointed types. This does not play a role in the rest of this paper, however.

3.3 The Baer Sum

The Baer sum is a binary operation on $\operatorname{Ext}^{1}(B,A)$ which makes it into an abelian group. Given two extensions $E,F:\operatorname{Ext}^{1}(B,A)$ their Baer sum is defined as

[TABLE]

where $E\oplus F$ is the point-wise direct sum, $\nabla(a,b):\equiv a_{0}+a_{1}:A\oplus A\to A$ is the codiagonal map, and $\Delta(b):\equiv(b,b):B\to B\oplus B$ is the diagonal map.

Together with Dan Christensen and Jacob Ender, we have implemented the Baer sum in Algebra.AbSES.BaerSum. We define this operation on the level of short exact sequences and then descend the operation to the set $\operatorname{{\verb~Ext~}}^{1}$ by truncation-recursion.♢

⬇

Definition abses_baer_sum ‘{Univalence} {B A : AbGroup}

: AbSES B A -> ABSES B A AbSES B A := fun E F =>

  abses_pullback ab_diagonal

    (abses_pushout ab_codiagonal (abses_direct_sum E F)).

Definition baer_sum ‘{Univalence} {B A : AbGroup}

: Ext B A -> Ext B A -> Ext B A.

Proof.

intros E F; strip_truncations.

exact (tr (abses_baer_sum E F)).

Defined.

Above, the strip_truncations tactic is a helper for doing truncation-recursion; it lets us assume that both $E$ and $F$ are elements of $\operatorname{{\verb~AbSES~}}(B,A)$ in order to map into the set $\operatorname{{\verb~Ext~}}^{1}(B,A)$. We then simply form the Baer sum of $E$ and $F$ on the level of short exact sequences before applying tr to the result.

The formalisation that the Baer sum makes $\operatorname{{\verb~Ext~}}^{1}(B,A)$ into an abelian group closely follows the “second proof” of [6, Theorem III.2.1].

Theorem 3.14**.**

The set $\operatorname{{\verb~Ext~}}^{1}(B,A)$ is an abelian group under the Baer sum operation.♢

The proof can be done entirely by chaining together equations once the bifunctoriality of $\operatorname{{\verb~Ext~}}^{1}$ has been established along with its interaction with direct sums. To illustrate this, we prove that pushouts respect the Baer sum:

Proposition 3.15**.**

Let $\alpha:A\to A^{\prime}$ be a homomorphism of abelian groups. For any abelian group $B$, pushout defines a group homomorphism $\alpha_{*}:\operatorname{{\verb~Ext~}}^{1}(B,A)\to\operatorname{{\verb~Ext~}}^{1}(B,A^{\prime}).$♢

Proof 3.16**.**

Using bifunctoriality of $\operatorname{{\verb~Ext~}}^{1}$ and naturality of $\oplus$, we have:

[TABLE]

Similarly, pullback defines a group homomorphism as well.♢ These results make $\operatorname{{\verb~Ext~}}^{1}$ into a bifunctor valued in abelian groups.♢

4 The Pullback Fibre Sequence

The main goal of this section is to explain and prove the following mathematical result, and to discuss its formalisation♢ along with some applications.

Theorem 4.1**.**

Let $A\xrightarrow{i}E\xrightarrow{p}B$ be a short exact sequence of abelian groups. For any abelian group $G$, pullback yields a fibre sequence: $\operatorname{{\verb~AbSES~}}(B,G)\xrightarrow{p^{*}}\operatorname{{\verb~AbSES~}}(E,G)\xrightarrow{i^{*}}\operatorname{{\verb~AbSES~}}(A,G).$♢

In [2, Proposition 2.3.2] we give a different proof of this result via an equivalence between $\operatorname{{\verb~AbSES~}}(B,A)$ and pointed maps between Eilenberg–Mac Lane spaces. However, this different proof seems to only work over $\operatorname{\mathbb{Z}}$ whereas our proof below works for a general ring (though it has only been formalised for $\operatorname{\mathbb{Z}}$).

A sequence of pointed maps $F\xrightarrow{i}E\xrightarrow{p}B$ is a fibre sequence if $p\circ i$ is pointed-homotopic to the constant map, and the induced map $F\to{\verb~fib~}_{p}$ is an equivalence. Any fibre sequence induces a long exact sequence of homotopy groups [10, Theorem 8.4.6]:

[TABLE]

In the situation of our theorem, it is immediate from functoriality and exactness of $E$ that $i^{*}\circ p^{*}$ is constant. Therefore our goal is to show that the induced map $c:\operatorname{{\verb~AbSES~}}(B,G)\to{\verb~fib~}_{i^{*}}$ is an equivalence.222The map $c$ is called cxfib in the code. We will do this by first constructing a section of $c$, and then a contraction of the fibres of $c$ to the values of this section. A key part of the formalisation is to work with path data instead of actual paths, since the former has better computational properties. We will simply use $E=F$ to denote path data, and refer to it as such, in this section.

Lemma 4.2**.**

Let $G\to F\to E$ be a short exact sequence. Given path data $p:i^{*}(F)=\operatorname{\verb~pt~}$, we construct a short exact sequence $G\to F/A\to B$.♢

Proof 4.3**.**

The path data $p$ means that the sequence $i^{*}(F)$ splits. Thus we can form the cokernel $F/A$ as in the diagram:

[TABLE]

The two maps $G\to F/A\to B$ are given by composition and the universal property of the cokernel, respectively. It is clear that this forms a complex and that the second map is an epimorphism, since it factors one. To see that the map $G\to F/A$ is an injection, suppose $g:G$ is sent to $0:F/A$. Then $j(g)$ is in the image of some $a:A$ by $A\to F$. But the map $i^{*}(F)\to F$ is an injection, being the pullback of one, and so using the path data we get an equality $(g,0)=(0,a)$ in $G\oplus A$. Of course, this implies that $g=0$, as required.

Exactness of $G\to F/A\to B$ follows from a straightforward diagram chase.

The diagram above exhibits $F$ as the pullback of $F/A$ along $p^{*}$, yielding:

Lemma 4.4**.**

We have path data $q:p^{*}(F/A)=F$.♢

Thus we have given a preimage $F/A$ of $F$ under $p^{*}$. To show that the fibre of $c$ is inhabited we will show that $c(F/A)=(F,p)$, which is a path in ${\verb~fib~}_{i^{*}}$. We express all of this in terms of path data, and such a path in ${\verb~fib~}_{i^{*}}$ then corresponds to path data $q:p^{*}(F/A)=F$ which makes the following triangle commute:♢

[TABLE]

where the rightmost map comes from $i^{*}p^{*}$ being trivial. The key reason we have formulated things in terms of path data is so that the maps in the triangle above simply compute, because they have all been concretely constructed.

In the following, $c$ refers to the map which lands in ${\verb~fib~}_{i^{*}}$ expressed in terms of path data.♢

Lemma 4.5**.**

We have $q:c(F/A)=(F,p)$ in ${\verb~fib~}_{i^{*}}$.♢

Proof 4.6**.**

The previous lemma already yields path data $q:p^{*}(F/A)=F$, thus it remains to show that the triangle in Equation 2 commutes. The way the maps have been constructed, it’s easiest to show this after flipping the triangle so that it starts at $G\oplus A$ and ends at $i^{*}p^{*}(F/A)$. (This is fine since all the maps are isomorphisms.) Thus we are comparing two maps out of a biproduct into a pullback. To check whether they are equal, we can check it on each inclusion of the biproduct and after projecting out of the pullback. In each of these cases one obtains diagrams which commute, but checking this is somewhat involved. Fortunately, by our having carefully crafted the path data involved, the maps simply compute and Coq is able to reduce the goal to a simple computation.

Combining the three previous lemmas, we get a section of $c:\operatorname{{\verb~AbSES~}}(B,G)\to{\verb~fib~}_{i^{*}}$. To conclude that $c$ is an equivalence, we contract each fibre over some $(F,p)$ to $(F/A,q)$.

Lemma 4.7**.**

Suppose $G\to Y\to B$ is a short exact sequence, and let $q^{\prime}:c(Y)=(F,p)$ in ${\verb~fib~}_{i^{*}}$. Then $(F/A,q)=(Y,q^{\prime})$ in the fibre of $c$ over $(F,p)$.♢

Proof 4.8**.**

Under our assumptions, we have the composite map $\phi:G\oplus A\to i^{*}p^{*}(Y)\to p^{*}(Y)$♢ which by a diagram chase can be seen to be the inclusion $G\to p^{*}(Y)$ on one component, and $(0,p):A\to p^{*}(Y)$ on the other.♢. Consequently, the composite $\verb~pr~_{1}\circ\phi\circ\verb~in~_{A}:A\to Y$ is trivial. By the universal property of the cokernel, we get an induced map $F/A\to Y$. Once again, by our careful construction of all the maps involved, it is straightforward to simply compute that this map defines path data $F/A=Y$ and moreover that this path lifts to a path in the fibre of $c$. There is a coherence between three paths in $\operatorname{{\verb~AbSES~}}(A,G)$ which is trivially satisfied, since $\operatorname{{\verb~AbSES~}}(A,G)$ is a $1$-type.

The final lemma implies that the fibres of $c$ are contractible, which means that $c$ is an equivalence and concludes the proof of Theorem 4.1. We now turn our attention to two applications of this theorem. The first application requires a lemma.

Lemma 4.9**.**

Let $g:B^{\prime}\to B$ be a homomorphism of abelian groups. For any $A$, the following diagram commutes, where the vertical isomorphisms are all given by Proposition 3.3:♢

[TABLE]

Proof 4.10**.**

Let $p:A\oplus B=A\oplus B$ be an element of the upper left corner, seen as path data. By path induction, one can easily show that the action of $\Omega(g^{*})$ on paths is given by pulling back the path data. (Formally, one first proves this for paths with free endpoints, then you can specialise to loops.) This means that the following diagram commutes

[TABLE]

where we have used the functions underlying the path data $p$ and $\Omega(g^{*})(p)$, and the unlabeled arrows are the natural ones into or out of a biproduct. The composites of the top and bottom rows above are the results of sending $p$ around the top-right and bottom-left corners of Diagram 3, respectively. Since this latter diagram commutes, so does Diagram 3.

Proposition 4.11** ([6, Theorem III.3.4]).**

We have an exact sequence of abelian groups:♢

[TABLE]

Proof 4.12**.**

This sequence comes from the long exact sequence of homotopy groups [10, Theorem 8.4.6] associated to the fibre sequence of Theorem 4.1, using Proposition 3.3 and the previous lemma to identify $\Omega\operatorname{{\verb~AbSES~}}(-,G)$ with $\operatorname{{\verb~Hom~}}(-,G)$.

Remark 4.13**.**

The connecting map $\operatorname{{\verb~Hom~}}(A,G)\to\operatorname{{\verb~Ext~}}^{1}(B,G)$ in the sequence above is given by $\phi\mapsto\phi_{*}E$. Showing this from the fibre sequence is somewhat tedious; we have a proof on paper, but not yet a formalisation. Instead, we have formalised a direct proof that the map just stated yields exactness of the sequence.♢♢

We apply the six-term exact sequence to compute Ext groups of cyclic groups:

Corollary 4.14** ([6, Proposition III.1.1]).**

For any $n>0$ and abelian group $A$, we have♢

[TABLE]

Proof 4.15**.**

The short exact sequence $\operatorname{\mathbb{Z}}\xrightarrow{n}\operatorname{\mathbb{Z}}\to\operatorname{\mathbb{Z}}/n$ yields a six-term exact sequence

[TABLE]

in which the term $\operatorname{{\verb~Ext~}}^{1}(\operatorname{\mathbb{Z}},A)$ vanishes since $\operatorname{\mathbb{Z}}$ is projective.♢♢ This means that the map $\operatorname{{\verb~Hom~}}(\operatorname{\mathbb{Z}},A)\to\operatorname{{\verb~Ext~}}^{1}(\operatorname{\mathbb{Z}}/n,A)$ is the cokernel of the preceding map. By identifying $\operatorname{{\verb~Hom~}}(\operatorname{\mathbb{Z}},A)$ with $A$, the claim follows.

5 The Long Exact Sequence

We describe our formalisation of the higher Ext groups $\operatorname{{\verb~Ext~}}^{n}(B,A)$ and their contravariant long exact sequence, which largely follows [6, Chapter III.5]. The covariant version can be constructed from the arguments in [7, Chapter VII.5], but we have not formalised this. The Baer sum is not yet formalised for $\operatorname{{\verb~Ext~}}^{n}$ $(n>1)$, so we only have a long exact sequence of pointed sets. Nevertheless, exactness for pointed sets and abelian groups coincide, so we automatically get a long exact sequence of the latter once we have the higher Baer sum.

The formalisation of this section is in the separate repository Yoneda-Ext, whose README file explains how to set up and build the code related to this chapter. There are also comments in the code which explain details beyond what we cover here.

5.1 The Type of Length-$n$ Exact Sequences

We start by defining a type $\operatorname{{\verb~ES~}}^{n}$ which we will equip with an equivalence relation by which $\operatorname{{\verb~Ext~}}^{n}$ will be the quotient. These constructions will yield functors, which we explain.

The type $\operatorname{{\verb~ES~}}^{n}(B,A)$ of length-$n$ exact sequences is recursively defined as:\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/ES.v#L16

⬇

Fixpoint ES (n : nat) : AbGroup^op -> AbGroup -> Type

:= match n with

| 0%nat => fun B A => Hom B A

| 1%nat => fun B A => AbSES B A

| S n => fun B A => exists M, (ES n M A) * (AbSES B M)

end.

Thus $\operatorname{{\verb~ES~}}^{0}(B,A)$ is definitionally $\operatorname{{\verb~Hom~}}(B,A)$, and $\operatorname{{\verb~ES~}}^{1}(B,A)$ is definitionally $\operatorname{{\verb~AbSES~}}(B,A)$. One could also have started the induction at $n\equiv 1$ instead of $n\equiv 2$, but it is convenient to have this definitional equality at level $n\equiv 1$. The functoriality of $\operatorname{{\verb~ES~}}^{n}$ is inherited from $\operatorname{{\verb~AbSES~}}$ and defined in the obvious way by pulling back and pushing out. For $n>0$, an element of $\operatorname{{\verb~ES~}}^{n+1}(B,A)$ is denoted by $(F,E)_{M}$, with the obvious meaning. The type \operatorname{{\verb~ES~}}^{n}(B,A)^{\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/ES.v#L32} is pointed by recursion, using the trivial abelian group in the place of $M$ in the inductive step.

Definition 5.1**.**

The splice operation is defined as{}^{\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/ES.v#L144}

[TABLE]

By induction one can define a general splicing operation in which the second parameter can have arbitrary length\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/ES.v#L166, but we only need the restricted version above.

Now we equip $\operatorname{{\verb~ES~}}^{n}(B,A)$ with a relation.

Definition 5.2**.**

We define a relation $\verb~es_zig~:\operatorname{{\verb~ES~}}^{n}(B,A)\to\operatorname{{\verb~ES~}}^{n}(B,A)\to\operatorname{\verb~Type~}$ recursively as follows. For $n=0,1$, es_zig is the identity type. For $n\geq 2$, a relation between two elements $(F,E)_{M}$ and $(Y,X)_{N}$ consists of a homomorphism $f:\operatorname{{\verb~Hom~}}(M,N)$ along with a path $f_{*}(E)=X$ and a relation $\verb~es_zig~(F,f^{*}(Y))$ (using functoriality of $\operatorname{{\verb~ES~}}^{n}$).\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/ES.v#L186

The relation es_zig generates an equivalence relation es_eqrel\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/ES.v#L224 (denoted ~ in the code) whose propositional truncation is es_meqrel\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/ES.v#L253. The functoriality of $\operatorname{{\verb~ES~}}^{n}$ respects these relations.\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/ES.v#L264\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/ES.v#L289 Basic results on equivalence relations are contained in EquivalenceRelation.v.

We emphasise that equivalence relation es_eqrel is not equivalent to the identity type of $\operatorname{{\verb~ES~}}^{n}$. Rather, it is an approximation of the identity type of the classifying space of the category $\operatorname{{\verb~ES~}}^{n}$ (which we do not know if one can construct in HoTT). See, e.g., [6, Chapter III.5] for related discussion.

Definition 5.3**.**

The pointed set $\operatorname{{\verb~Ext~}}^{n}(B,A)$ is the quotient of $\operatorname{{\verb~ES~}}^{n}(B,A)$ by the equivalence relation es_meqrel.\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/HigherExt.v#L15

The splice operation descends to this quotient.\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/HigherExt.v#L96 By pushing out\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/HigherExt.v#L80 and pulling back\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/HigherExt.v#L65 extensions, $\operatorname{Ext}^{n}$ becomes a functor in each variable as well. Moreover, we have equalities $f^{*}(F)\operatorname{\circledcirc}E=F\operatorname{\circledcirc}f_{*}(E)$ whenever this expression makes sense, by the definition of es_zig.\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/HigherExt.v#L140

Remark 5.4**.**

The definition of $\operatorname{{\verb~Ext~}}^{n+1}(B,A)$ is, more conceptually, the $(n+1)$-fold tensor product of functors $\operatorname{{\verb~Ext~}}^{n+1}(B,A)=\operatorname{{\verb~Ext~}}^{n}(-,A)\otimes\operatorname{{\verb~Ext~}}^{1}(B,-)$ (see, e.g., [5, Theorem 9.20] or [13, Eq. 4.3.4]). In our setup, this is a tensor product of Set-valued functors, which can be made into an abelian group by a construction similar to the Baer sum of Section 3.3 (though we have not yet formalised this). Alternatively, one could define $\operatorname{{\verb~Ext~}}^{n+1}(B,A)$ as the $(n+1)$-fold tensor product of functors into abelian groups. [4, Lemma 2.1] implies that these two definitions coincide. We have chosen the present approach because we do not know of a direct construction of the long exact sequence for the latter approach.

5.2 The Long Exact Sequence

We now begin working towards the long exact sequence, following the proof of [6, Theorem XII.5.1]. As explained at the beginning of this section, we have only formalised the long exact sequence of pointed sets—however, exactness for pointed sets is the same as for abelian groups. Let us first recall the statement:

Theorem 5.5**.**

Let $A\xrightarrow{i}E\xrightarrow{p}B$ be a short exact sequence of abelian groups. For any abelian group $G$, there is a long exact sequence by pulling back:\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/LES.v#L15\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/LES.v#L47\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/LES.v#L94

[TABLE]

The proof in [6] first discusses the six-term exact sequence, which we proved as Proposition 4.11. It then reduces the question to exactness at the domain of the connecting map (Lemma XII.5.2, loc. cit.), and proves exactness at that spot using Lemmas XII.5.3, XII.5.4, and XII.5.5. We will show the three latter lemmas, then directly prove exactness at the other spots, essentially “in-lining” Lemma XII.5.2.

The various constructions we need to do are simpler to carry out on the level of $\operatorname{{\verb~ES~}}^{n}$ as opposed to $\operatorname{{\verb~Ext~}}^{n}$. For this reason we work and formulate things in terms of the former, and then deduce the desired statement for the latter.

Before attacking Lemma XII.5.3, we show the following:

Lemma 5.6**.**

Consider two pairs of short exact sequences which can be spliced:

[TABLE]

For any element of $\verb~es_zig~(Y\operatorname{\circledcirc}X,F\operatorname{\circledcirc}E)$, we have induced maps {\verb~fib~}_{s_{*}}(X)\to{\verb~fib~}_{q_{*}}(E)\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/XII_5.v#L45 and {\verb~fib~}_{i^{*}}(F)\to{\verb~fib~}_{k^{*}}(Y)\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/XII_5.v#L82.

Proof 5.7**.**

We only describe the first map since the second is analogous. The zig from $Y\operatorname{\circledcirc}X$ to $F\operatorname{\circledcirc}E$ gives a homomorphism $f:B^{\prime}\to B$ along with two paths $f^{*}(F)=Y$ and $f_{*}(X)=E$. Let $G:{\verb~fib~}_{s_{*}}(X)$; by path induction we may assume $q_{*}(G)\equiv X$. The path $f^{*}(F)=Y$ means we have a commuting diagram:

[TABLE]

Thus $\phi_{*}(G)$ defines an element of ${\verb~fib~}_{q_{*}}(E)$ by $q_{*}(\phi_{*}(G))=f_{*}(s_{*}(G))\equiv f_{*}(X)=E.$

Lemma 5.8** ([6, Lemma XII.5.3]).**

Given two short exact sequences $A\xrightarrow{j}F\xrightarrow{q}B$ and $B\xrightarrow{i}E\xrightarrow{p}C$, the following types are logically equivalent:\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/XII_5.v#L173

${\verb~fib~}_{i^{*}}(F)$; 2. 2.

${\verb~fib~}_{q_{*}}(E)$; 3. 3.

$\verb~es_eqrel~(\operatorname{\verb~pt~},F\operatorname{\circledcirc}E)$.

Proof 5.9**.**

The logical equivalence of between (1) and (2) is as described in [6].\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/XII_5.v#L131 Moreover, the implication (2) to (3) is clear by the definition of es_zig. We need to show that (3) implies (1), and we proceed by induction on the length of the zig-zag.

In the base case we have an actual equality $\operatorname{\verb~pt~}=F\operatorname{\circledcirc}E$, in which case (1) clearly holds. For the inductive step, suppose we have two short exact sequences $A\xrightarrow{l}Y\xrightarrow{s}B^{\prime}$ and $B^{\prime}\xrightarrow{k}X\xrightarrow{r}C$ such that $Y\operatorname{\circledcirc}X$ is related to $\operatorname{\verb~pt~}$ by a length $n$ zig-zag, and we have either zig or a zag relating $Y\operatorname{\circledcirc}X$ to $F\operatorname{\circledcirc}E$. If we have a zig, then we use the induction hypothesis to get an element of ${\verb~fib~}_{s_{*}}(X)$ to which we apply the map ${\verb~fib~}_{s_{*}}(X)\to{\verb~fib~}_{q_{*}}(E)$ from the previous lemma. This suffices since (1) and (2) are logically equivalent.

If we have a zag, then the previous lemma gives a map ${\verb~fib~}_{k^{*}}(Y)\to{\verb~fib~}_{i^{*}}(F)$, so we are done by the induction hypothesis.

We reformulate condition (2) in a manner that generalises to $\operatorname{{\verb~ES~}}^{n}$.\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/XII_5.v#L214

⬇

Definition es_ii_family ‘{Univalence} {n : nat} {C B A : AbGroup}

: ES n.+1 B A -> ES 1 C B -> Type

:= fun E F => { alpha : { B’ : AbGroup & B’ $-> B }

                   & (es_eqrel pt (es_pullback alpha.2 E))

                     * (hfiber (abses_pushout alpha.2) F) }.

Lemma 5.10** ([6, Lemma XII.5.4]).**

In the situation of the previous lemma, the types ${\verb~fib~}_{q_{*}}(E)$ and $\verb~es_ii_family~(F,E)$ are logically equivalent.\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/XII_5.v#L221

Mac Lane appeals to the six-term exact sequence to prove this lemma, but we give a direct construction. In order to show Lemma XII.5.3, we prove a higher analogue of Lemma 5.6. This analogue is phrased in terms of the “relation fibre” rfiber, which takes the fibre of a point with respect to a relation.

Lemma 5.11**.**

Let $n>0$ and consider $Y:\operatorname{{\verb~ES~}}^{n}(B^{\prime},A)$, $F:\operatorname{{\verb~ES~}}^{n}(B,A)$, and two short exact sequences $B^{\prime}\xrightarrow{k}X\to C$ and $B\xrightarrow{i}E\to C$. Given $\verb~es_zig~(Y\operatorname{\circledcirc}X,F\operatorname{\circledcirc}E)$, we have maps \verb~rfiber~_{i^{*}}(F)\to\verb~rfiber~_{k^{*}}(Y)\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/XII_5.v#L285 and \verb~es_ii_family~(Y,X)\to\verb~es_ii_family~(F,E)\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/XII_5.v#L266.

Lemma 5.12** ([6, Lemma XII.5.5]).**

Let $n>0$, $F:\operatorname{{\verb~ES~}}^{n}(B,A)$, and $E:\operatorname{{\verb~ES~}}^{1}(C,B)$. The following types are equivalent:\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/XII_5.v#L375

${\verb~fib~}_{i^{*}}(E)$; 2. 2.

$\verb~es_ii_family~(F,E)$; 3. 3.

$\verb~es_eqrel~(\operatorname{\verb~pt~},F\operatorname{\circledcirc}E)$.

Proof 5.13**.**

We first prove an auxiliary lemma which shows that if the three statements are equivalent for a given $n$, then (1) and (2) are equivalent for $n+1$. The base case for this lemma is simply Lemma 5.8. For the inductive step, our auxiliary lemma gives us that (1) and (2) are equivalent. It is easy to show that (2) always implies (3), so it remains to show that (3) implies either (1) or (2). For this we induct on the length of a zig-zag, and use the equivalence of (1) and (2) along with the previous lemma, similarly (at least in structure) to the proof of Lemma 5.8.

Afterwards, we reformulate this lemma in terms of $\operatorname{{\verb~Ext~}}^{n}$.\href https://github.com/jarlg/Yoneda-Ext/blob/0d8bfe8e168bbdf325e805d7268e826e889189f0/XII_5.v#L505 With this lemma at hand, and using similar methods to the ones presented here, we follow the proof of [6, Lemma 5.2] to deduce exactness of the long sequence of Theorem 5.5.

6 Conclusion

We have presented a formalisation of the theory of Yoneda Ext in the novel setting of homotopy type theory, starting from the basic definition of a short exact sequence and arriving at the (contravariant) long exact sequence, with various related results along the way. At present, the long exact sequence is one of pointed sets, and we leave it to future work to formalise the Baer sum on $\operatorname{{\verb~Ext~}}^{n}$ for $n>1$, which would promote this into a long exact sequence of abelian groups. (The notion of exact sequence coincides for abelian groups and pointed sets.)

For pragmatic reasons we have worked with abelian groups, though it is clear that everything we have done could be applied to general modules. Even so, the higher Ext groups of abelian groups do not necessarily vanish in HoTT [2], so these are already interesting. There are various more general approaches that we would like to consider in the future, such as working with pure exact sequences (in which the classes of monomorphisms and epimorphisms are appropriately replaced) in an abelian category.

Many of our results have been contributed to the Coq-HoTT library [3] under the namespace Algebra.AbSES, which currently weighs in at about 2900 lines of code (whitespace and comments included). This excludes the various contributions made to other parts of the library; the precise contributions may be seen through the pull requests #1534, #1646, #1663, #1712, #1718, and #1738. In addition, the code for the long exact sequence currently weighs in at about 1350 lines in the separate Yoneda-Ext repository.

The formalisation covers a substantial part of chapters III.1-3, III.5, and XII.5 of [6], but also extends beyond the classical theory. In particular, our proof of Theorem 4.1 is new even for classical Yoneda Ext (though the theorem is known). This theorem presented the most challenging part of this formalisation, as it required managing considerable amounts of coherence. The other challenging part was the long exact sequence, whose proof involves an intricate induction and numerous constructions. By formalising these theorems we have not only established their correctness but also contributed evidence of the feasibility of dealing with sophisticated mathematical structures in a proof assistant like Coq.