How to make Ext and Tor constructive?

Question

EDIT: This post was substantially modified with the help of the comments and answers. Thank you!

---

Judging by their definitions, the $\mathrm{Ext}$ and $\mathrm{Tor}$ functors are among the most non-constructive things considered in algebra:

(1) Their very definition requires taking an infinite projective or injective resolution; constructing a homotopy equivalence between two such resolutions requires infinitely many choices.

(2) Injective resolutions are rather problematic in a constructive world (e. g. the proof of "injective = divisible" requires Zorn, and as far as I understand the construction of an injective resolution relies on this fact).

(3) Projective/injective resolutions are not really canonical, so $\mathrm{Ext}$ and $\mathrm{Tor}$ are not functors from "pairs of modules" to "groups", but rather functors from "pairs of modules" to some category between "groups" and "isomorphism classes of groups". This is a problem already from the classical viewpoint.

(4) Projective resolutions are not guaranteed to exist in a constructive world, because the free module on a set needs not be projective! In order to avert this kind of trouble, we could try restricting ourselves to very well-behaved modules (such as, finite-dimensional over a field), but even then we are in for a bad surprise: Sometimes, the "best" projective resolution for a finitely-generated module uses non-finitely-generated projective modules (I will show such an example further below). These can be tricky to deal with, constructively. Mike Shulman has mentioned (in the comments) that injective and projective resolutions (and already the proofs that the different definitions of "projective" are equivalent, and that the different definitions of "injective" are equivalent) require choice - maybe the currently accepted notions of injectivity and projectivity are not "the right one" except for finitely-generated modules? (Cf. also this here.)

On the other hand, if we think about the ideas behind $\mathrm{Ext}$ and $\mathrm{Tor}$ and projective resolutions (I honestly don't know the ideas behind injective resolutions, besides to dualize the notion of projective resolutions), they are (at least partially) inspired by some of the most down-to-earth constructive mathematics, namely syzygy theory. So a natural question to pose is: How can we implement the theory of $\mathrm{Ext}$ and $\mathrm{Tor}$, or at least a part of this theory which still has the same applications as the whole theory, without having to extend our logical framework beyound constructivism?

It is not hard to address the issues (1), (2), (3) above one at a time, at least when it comes to the basic properties of $\mathrm{Ext}$ and $\mathrm{Tor}$:

For (1), the workaround is easy: If you want $\mathrm{Ext}^n\left(M,N\right)$ for two modules $M$ and $N$ and some $n\in\mathbb N$, you don't need a whole infinite projective resolution $...\to P^2\to P^1\to P^0\to M$. It is enough to have an exact sequence $P^{n+1}\to P^n\to P^{n-1}\to ...\to P^1\to P^0\to M$, where $P^0$, $P^1$, ..., $P^n$ are projective. (It is not necessary for $P^{n+1}$ to be projective. Generally, $P^{n+1}$ is somewhat like a red herring when $\mathrm{Ext}^n\left(M,N\right)$ is concerned.)

For (2), the only solution I know is not to use injective resolutions. Usually, things that can be formulated with projective resolutions only can also be proven with projective resolutions only. But this is not a solution I like, since it breaks symmetry.

(3) I think this is what anafunctors are for, but I have not brought myself to read the ncatlab article yet. I know, laziness is an issue... At the moment, I am solving this issue in a low-level way: Never speak of $\mathrm{Ext}\left(M,N\right)$, but rather speak of $\mathrm{Ext}\left(M_P,N\right)$ or $\mathrm{Ext}\left(M,N_Q\right)$, where $P$ and $Q$ are respective projective/injective resolutions. This seems to be the honest way to do work with $\mathrm{Ext}$'s anyway, because once you start proving things, these resolutions suddenly do matter, and you find yourself confused (well... I find myself confused) if you suppress them in the notation. [Note: If you want to read Makkai's lectures on anafunctors and you are tired of the Ghostview error messages, remove the "EPSF-1.2" part of the first line of each of the PS files.]

Now, (4) is my main problem. I could live without injective resolutions, without the fake canonicity of $\mathrm{Ext}$ and $\mathrm{Tor}$, and without infinite projective resolutions, but if I am to do homological algebra, I can hardly dispense with finite-length projective resolutions! Unfortunately, as I said, in constructive mathematics, there is no guarantee that a module has a projective resolution at all. The standard way to construct a projective resolution for an $R$-module $M$ begins by taking the free module $R\left[M\right]$ on $M$-as-a-set - or, let me rather say, $M$-as-a-type. Is this free module projective, constructively? This depends on what we know about $M$-as-a-type. Alas, in general, modules considered in algebra often have neither an obvious set of generators nor an a-priori algorithm for membership testing; they can be as complicated as "the module of all $A$-equivariant maps from $V$ to $W$" with $A$, $V$, $W$ being infinite-dimensional. Some are even proper classes, even in the classical sense. The free module over a discrete finite set is projective constructively, but the free module over an arbitrary type does so only if we allow a weaker form of AC through the backdoor. Anyway, even if there is a projective resolution, it cannot really be used for explicit computations if the modules involved are not finitely generated. Now, here is an example of where non-finitely generated modules have an appearance:

Theorem. If $R$ is a ring, then the global homological dimension of the polynomial ring $R\left[x\right]$ is $\leq$ the global homological dimension of $R$ plus $1$.

I am referring to the proof given in Crawley-Boevey's lecture notes. (Look at page 31, absatz (2).) For the proof, we let $M$ be an $R\left[x\right]$-module, and we take the projective resolution

$0 \to R\left[x\right] \otimes_R M \to R\left[x\right] \otimes_R M \to M \to 0$,

where the second arrow sends $p\otimes m$ to $px\otimes m-p\otimes xm$, and the third arrow sends $q\otimes n$ to $qn$. (This is a particular case of the standard resolution of a representation of a quiver, which appears on page 7 of a different set of lecture notes by the same Crawley-Boevey.)

Now, the problem is that even if $M$ is finitely generated as an $R\left[x\right]$-module, $R\left[x\right] \otimes_R M$ needs not be.

Is there a known way around this?

Generally, what is known about constructive $\mathrm{Ext}$/$\mathrm{Tor}$ theory? Are there texts on it, just as Lombardi's one on various other parts of algebra (strangely, this text talks a lot about projective modules, but gives $\mathrm{Ext}$ and $\mathrm{Tor}$ a wide berth)? Do the problems dissolve if I really use anafunctors? Do derived categories help? Should we replace our notions of "injective" and "projective" by better ones? Or is there some deeper reason for the non-constructivity, i. e. is $\mathrm{Ext}$/$\mathrm{Tor}$ theory too strong?

---

Endnote for everyone who does not care about constructive mathematics: Even dropping constructivism aside, I believe that there remain quite a lot of real issues with homological algebra. First there is the matter of canonicity, then there is the problem of too-big constructions (proper classes etc.), the frightening unapproachability of injective covers, the idea that one day we might want to work in a topos where even ZF is too much asked, etc. I am changing the topic to a discussion of how to fix these issues (well, it already is such a discussion), constructivism being just one of the many directions to work in.

Answer 1

I have some sympathy for the question, since I have gotten bothered by the noncanoncity -- although less so by the nonconstructivity -- of the usual definition in my youth. (These days I'm less bothered by such things.) Here are a few ways around it for $Ext$.

1. There is a definition going back Yoneda, I think, of $Ext^n(M,N)$ as an equivalence class of exact sequences $0\to N\to \ldots \to M\to 0$ of length $n+2$ (including $M,N$). Take a look at Hilton and Stammbach's Homological Algebra. This is quite cumbersome but it solves the dependency on, let alone existence of, suitable resolutions.

2. This was mentioned already by Mike Shulman. You can take $Ext^n(M,N)= Hom_{D(R)}(M,N[n])$ in the derived category $D(R)$ of $R$-modules. Once you get used to the formalism, this is much more convenient than 1 (at least for me).

3. You can choose a canonical resolution initially for the definition of $Ext^n(M,N)$. Here is one general choice. Let $F^0(M)=F(M)$ be the free module generated by elements of $M$. We have canonical map $c_M:F(M)\to M$, let $F^{-1}(M)= F(\ker c_M)$. By continuing in this fashion, we build a canonical free resolution $\ldots F^{-1}(M)\to F^0(M)\to M\to 0$. Dually, you can use the injective hull* to build an injective resolution of $N$. As several people have pointed out, some important categories have enough injectives but not enough projectives, so it's good to get used to them.

Addendum Regarding your original question about how constructive this can be made, I think for certain classes of modules (e.g. finitely presented modules) over certain classes of rings (e.g. polynomial rings), this is not only possible, but it seems to have been implemented in some computer algebra packages already. I notice that the latest Macaulay 2 has commands for Ext and Tor.

*If your are unhappy with this, use instead the double character module $$I(N)= Hom_{\mathbb{Z}}(Hom_{\mathbb{Z}}(N,\mathbb{Q}/\mathbb{Z}), \mathbb{Q}/\mathbb{Z})$$

Answer 2

Jarl Flaten and I have developed the theory of Ext groups constructively in homotopy type theory, and have formalized most of the results in Coq. We use Yoneda's resolution-free approach to Ext, so there are no choices involved in the definition, and it works even in models in which there are not enough projective or injective R-modules. We prove the standard long exact sequences, and show that when you do have resolutions, you use them to compute Ext.

While we haven't worked through the details, you can use Ext to define other derived functors, including Tor. The derived functors of a covariant right exact functor $T$ can be defined as $$ T_n(C) := \operatorname{nat.trans.}(\operatorname{Ext}^n(C,-), T(-)). $$ This is due to Yoneda (1960), and is briefly described in the notes to Chapter XII of Mac Lane's Homology.

References:

J. Daniel Christensen and Jarl G. Taxerås Flaten. Ext groups in homotopy type theory. https://arxiv.org/abs/2305.09639

Jarl G. Taxerås Flaten. Formalising Yoneda Ext in Univalent Foundations. https://arxiv.org/abs/2302.12678

Slides for a talk I gave are available at https://jdc.math.uwo.ca/papers.html

Formalization: https://github.com/HoTT/Coq-HoTT and https://github.com/jarlg/Yoneda-Ext

Answer 3

Perhaps constructively it is misguided to expect Tor and Ext to be definable in terms of a single resolution.

One way to define Ext(M,N) is as the homology groups of DHom(M,N) in the derived category of chain complexes. The derived category of chain complexes is obtained from the category of chain complexes by inverting quasi-isomorphisms. In the presence of projective or injective resolutions, the category of chain complexes has a (projective or injective) Quillen model structure so that DHom(M,N) can be computed as Hom(QM,N) or Hom(M,RN) for a projective (= cofibrant) resolution QM or an injective (= fibrant) resolution RN.

In the absence of resolutions, it seems likely to me that the "right" thing to look at would still be DHom(M,N); it would just be harder to compute. A priori you would have to look at arbitrary zigzags of chain complexes, with backwards-pointing maps being quasi-isomorphisms. But it might still happen that there is a calculus of fractions or something that would reduce it to two- or three-step zigzags that you have to look at. But you would still then have to use different "resolutions" to represent different elements of Ext(M,N).

This is all based on general nonsense intuition, however, not on any experience of actually trying to do anything with Tor and Ext constructively, so it could be way off.

Answer 4

This is not exactly what you're asking, but computationally there is no problem with Ext and Tor over finitely-generated commutative algebras over a field. The algorithms are described in Eisenbud's commutative algebra book, as well as other places. For schemes, you can use the Cech definitions. I don't know to what extent these depend on choice to prove that they compute the right thing, since the theory relies on injective resolutions at various points, even though they are avoidable in calculations.

It seems to me that you could constructively handle injective modules the same way that you constructively handle the algebraic closure of a field. (Does the existence of the algebraic closure of $\mathbb{Q}$ require choice?) I don't think you literally need the whole injective module, just as in the way you usually don't literally need the whole algebraic closure of a ring. You adjoin roots of polynomials/solutions of linear equations as necessary. I don't know if you can give a constructive proof that this stops, though.

Answer 5

I am no authority on what I'm about to write, but the nLab discusses a weakened form of the axiom of choice called COSHEP (the Category Of Sets Has Enough Projectives), aka the Presentation Axiom (PAx) that some constructivists apparently consider reasonable. The principle does indeed hold for various models of intuitionistic set theory, for example any presheaf topos and also the effective topos, where the full axiom of choice fails badly.

Under COSHEP, it is easy to construct projective resolutions in algebra. And apparently this is a main application for constructive mathematicians, so the question raised by Darij has certainly been considered in the literature.

As regards injective resolutions: isn't the situation in Grothendieck toposes rather better than for projective resolutions? I am thinking here that a primary mathematical justification for interest in constructive proofs is that they admit a much wider semantic range than classical proofs. In particular, the internal logic of a topos is 'constructive', and a primary reason one is interested in constructive proofs is that they tend to carry over to toposes. Anyway, if I'm not too badly informed, the category of abelian group objects in a Grothendieck topos always has enough injectives; it may not have enough projectives however. Indeed, the interest in things like "flabby sheaves" seems to come down squarely on the injective side. (Hm, just noticed that Greg Friedman made a similar point in a comment above.)

All that being said, I expect that to push "enough injectives" through to Grothendieck toposes, one must assume certain baseline choice principles on the base topos $Set$. The "enough injectives" result on Grothendieck toposes probably hinges on some external considerations (like the existence of a generator) rather than internal logical considerations, so I'm a little murky on what constructivism really has to say here. All I'm saying above is that if your primary interest in constructive proofs is that they carry over to Grothendieck toposes, then fear not: they have enough injectives already.

I'm hoping that someone such as Andreas Blass will weigh in here at some point.