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.

  • 4
    $\begingroup$ Regarding injective and projective resolutions constructively, you may be interested in the paper Injectivity, projectivity, and the axiom of choice by Andreas Blass. $\endgroup$ Jan 3, 2011 at 0:32
  • 10
    $\begingroup$ There is a constructive (even functorial) resolution using a 2-sided bar construction that works for any ring R with module M. (It uses the forgetful-free adjoint pair between R-modules and sets.) If you define it using this horribly impractical definition, there is no indeterminacy and the "standard" definitions become theorems about ways to compute Tor. $\endgroup$ Jan 3, 2011 at 0:55
  • 5
    $\begingroup$ But there seems to be a lingering issue that frees might not be projective in the absence of choice. $\endgroup$
    – Todd Trimble
    Jan 3, 2011 at 2:05
  • 5
    $\begingroup$ @Theo B: why do those huge free modules require choice? I thought there was a canonical basis for them (like the underlying set of $M\times N$). That gives you the tensor product of abelian groups; then the tensor product of R-modules is just a coequalizer in Ab. $\endgroup$ Jan 3, 2011 at 6:16
  • 3
    $\begingroup$ This is a good idea, because I like Gröbner bases... but as far as I know, Gröbner bases work over a field only. Constructively, fields are extremely rare (e. g. we can't construct a splitting field, and we can't make a ring into a field by dividing by a maximal ideal), but I guess some of the ideas will be very useful. $\endgroup$ Jan 5, 2011 at 13:48

5 Answers 5


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})$$

  • $\begingroup$ Thanks a lot. I have heard of 1, although this creates a new problem (namely, $\mathrm{Ext}$ becomes a proper class), and doesn't work for $\mathrm{Tor}$ (not even for $\mathrm{Tor}^0$, which is reflected by the fact that the tensor product is the most difficult to understand thing in linear algebra). As for 2, I am trying to get used to derived categories; ATM I can't prove that this definition is equivalent to the usual one however. 3 is what Tyler proposed, and what I am currently using. $\endgroup$ Jan 3, 2011 at 17:29
  • 1
    $\begingroup$ However, injective hulls are not as canonical, as far as I understand, so 3 really works only for the projective part of the theory. $\endgroup$ Jan 3, 2011 at 17:30
  • 2
    $\begingroup$ Yes, I agree, these approaches solves some problems and creates others. Incidentally, whenever I teach sheaf cohomology, I use Godement's canonical flasque resolutions and avoid injectives altogether (and before anyone says anything, I know this won't work for arbitrary topoi...). $\endgroup$ Jan 3, 2011 at 17:38
  • 3
    $\begingroup$ @Donu, that won't work for arbtrary --- oops, you anticipated me... :-) $\endgroup$
    – Ravi Vakil
    Jul 21, 2011 at 22:33
  • 5
    $\begingroup$ @darijgrinberg [I have heard of 1, although this creates a new problem (namely, Ext becomes a proper class)] As long as you consider only modules of finite type over a noetherian ring $A$, you can define $Ext_A^n(M, N)$ as a set of equivalence classes on a set, because a module of finite type over $A$ is isomorphic to $A^m/R$, where $R$ is a submodule of $A^m$. $\endgroup$ May 1, 2014 at 11:49

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.

  • 1
    $\begingroup$ Thanks: even if this doesn't answer my question, it provides me a lot to think and read about. ;) I am a bit scared of derived categories: with the definition I know, the derived category of a locally small but not small category is not even locally small anymore, so there seems to be some inherent evil in that notion which should be exorcised first (in the fires of type theory?...). Now I have done enough rambling for 10 soft-questions, so I guess I should stop. Thanks again for all the help. $\endgroup$ Jan 3, 2011 at 1:13
  • 4
    $\begingroup$ It's true that if you take a locally-small non-small category and invert some weak equivalences, the result may no longer be locally small. I would guess that local-smallness of the derived category of a ring requires a weak form of choice (similar to nlab.mathforge.org/nlab/show/WISC). I'm not sure what's evil about non-locally-small categories, though. $\endgroup$ Jan 3, 2011 at 4:07

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.


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

  • $\begingroup$ Beautiful! Will have a read. $\endgroup$
    – ಠ_ಠ
    May 27, 2023 at 2:33

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.

  • 1
    $\begingroup$ The existence and uniqueness of algebraic closures can be deduced from the ultrafilter lemma, so doesn't require the full power of choice: see mathoverflow.net/questions/46566/… . In the specific case of Q, doesn't the proof that C is algebraically closed go through in ZF? Then we can just take the algebraic numbers in C. $\endgroup$ Jan 3, 2011 at 18:57
  • $\begingroup$ @Qiaochu: In ZF, I believe so, but constructively, I don't think you can even prove that the real numbers are real-closed: the intermediate value theorem requires some LEM. $\endgroup$ Jan 3, 2011 at 20:45
  • $\begingroup$ The "just adjoin roots as necessary" sounds similar to what I suggested about needing to use different "resolutions" to represent different morphisms in the derived category? $\endgroup$ Jan 3, 2011 at 20:47
  • $\begingroup$ That's a good point. You could work with chain complexes that are quasi-isomorphic to the original module, such that the first module in the complex is an essential extension of the original module, and each additional module is the complex is an essential extension of the previous one. Now we just need to prove that we can get every morphism of the derived category that way... $\endgroup$
    – arsmath
    Jan 3, 2011 at 22:52
  • 1
    $\begingroup$ @Qiaochu: I believe: Constructively (without any form of choice), the complex numbers built as pairs of Cauchy real numbers are algebraically closed, but the complex numbers built as pairs of Dedekind real numbers might not. (The former embed into the latter.) The algebraic numbers, defined as a subset of either kind of complex numbers, are always algebraically closed. They're also preserved by inverse image under geometric morphisms. $\endgroup$ Jun 7, 2018 at 11:35

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.

  • 1
    $\begingroup$ My primary interest in constructive proofs is that they are constructive, and alas I don't know what a topos is. This is going to change when I have something like a month of spare time for reading Barr's TTT book. Unfortunately, I have no idea when this is going to be. To be honest, I have NO idea why free modules are not projective constructively, so it seems like confusion has got the better of me now. $\endgroup$ Jan 3, 2011 at 14:08
  • $\begingroup$ Thanks for the reply, the mention of COSHEP seems to explain some things. $\endgroup$ Jan 3, 2011 at 14:10
  • 1
    $\begingroup$ @Darij: A detailed introduction into topos theory takes months or even years to read, I think. As a first introduction, you might check out maths.gla.ac.uk/~tl/cafe_topos_intro.pdf $\endgroup$ Jan 3, 2011 at 15:22
  • 2
    $\begingroup$ @Darij: perhaps you've got it sorted out by now, but you just have to work through the usual element-chasing proofs that free modules are projective to see where AC comes in. "Given f: P --> X, P free, and an epi p: Y --> X, I have to lift f through p. Let e_i be a basis of P; the lift should take e_i to some y which maps down to p(y). So I need to choose such y etc." It's hard to do this without some form of choice. $\endgroup$
    – Todd Trimble
    Jan 3, 2011 at 16:02
  • 1
    $\begingroup$ I see, this depends on what we mean by a "surjection". For me, a map $f:X\to Y$ (of sets) is called a surjection if and only if for every $y\in Y$, there exists an $x\in X$ such that $f(x)=y$. Now, "for every" is, type-theoretically, a lambda abstraction, so if I know that "for every $y\in Y$, there exists an $x\in X$ such that $f(x)=y$", then I actually have a map $g:Y\to X$ which assigns to each $y\in Y$ an $x\in X$ satisfying $f(x)=y$. Now, this has an ugly consequence, namely that if $X$ is a set and $\sim$ is an equivalence relation on $X$, then the canonical projection ... $\endgroup$ Jan 3, 2011 at 17:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.