Algorithm or theory of diagram chasing One of the standard parts of homological algebra is "diagram chasing", or equivalent arguments with universal properties in abelian categories.  Is there a rigorous theory of diagram chasing, and ideally also an algorithm?
To be precise about what I mean, a diagram is a directed graph $D$ whose vertices are labeled by objects in an abelian category, and whose arrows are labeled by morphisms.  The diagram might have various triangles, and we can require that certain triangles commute or anticommute.   We can require that certain arrows vanish, which can be used to ask that certain compositions vanish.  We can require that certain compositions are exact.  Maybe some of the arrows are sums or direct sums of other arrows, and maybe some of the vertices are projective or injective objects.  Then a diagram "lemma" is a construction of another diagram $D'$, with some new objects and arrows constructed from those of $D$, or at least some new restrictions.
As described so far, the diagram $D$ can express a functor from any category $\mathcal{C}$ to the abelian category $\mathcal{A}$.  This looks too general for a reasonable algorithm.  So let's take the case that $D$ is acyclic and finite.  This is still too general to yield a complete classification of diagram structures, since acyclic diagrams include all acyclic quivers, and some of these have a "wild" representation theory.  (For example, three arrows from $A$ to $B$ are a wild quiver.  The representations of this quiver are not tractable, even working over a field.)  In this case, I'm not asking for a full classification, only in a restricted algebraic theory that captures what is taught as diagram chasing.
Maybe the properties of a diagram that I listed in the second paragraph already yield a wild theory.  It's fine to ditch some of them as necessary to have a tractable answer.  Or to restrict to the category $\textbf{Vect}(k)$ if necessary, although I am interested in greater generality than that.
To make an analogy, there is a theory of Lie bracket words.  There is an algorithm related to Lyndon words that tells you when two sums of Lie bracket words are formally equal via the Jacobi identity.  This is a satisfactory answer, even though it is not a classification of actual Lie algebras.  In the case of commutative diagrams, I don't know a reasonable set of axioms — maybe they are related to triangulated categories — much less an algorithm to characterize their formal implications.
(This question was inspired by a mathoverflow question about George Bergman's salamander lemma.)

David's reference is interesting and it could be a part of what I had in mind with my question, but it is not the main part.  My thinking is that diagram chasing is boring, and that ideally there would be an algorithm to obtain all finite diagram chasing arguments, at least in the acyclic case.  Here is a simplification of the question that is entirely rigorous.
Suppose that the diagram $D$ is finite and acyclic and that all pairs of paths commute, so that it is equivalent to a functor from a finite poset category $\mathcal{P}$ to the abelian category $\mathcal{A}$.  Suppose that the only other decorations of $D$ are that: (1) certain arrows are the zero morphism, (2) certain vertices are the zero object, and (3) certain composable pairs of arrows are exact.  (Actually condition 2 can be forced by conditions 1 and 3.)  Then is there an algorithm to determine all pairs of arrows that are forced to be exact?  Can it be done in polynomial time?
This rigorous simplification does not consider many of the possible features of lemmas in homological algebra.  Nothing is said about projective or injective objects, taking kernels and cokernels, taking direct sums of objects and morphisms (or more generally finite limits and colimits), or making connecting morphisms.  For example, it does not include the snake lemma.  It also does not include diagrams in which only some pairs of paths commute.  But it is enough to express the monomorphism and epimorphism conditions, so it includes for instance the five lemma.
 A: Here's an attempt, assuming the target category is finite dimensional vector spaces and the diagram is finite acyclic.
1)  Fill in the diagram so it's triangulated (that is, add the compositions of all arrows).  Add kernels and cokernels to every arrow in the diagram.  Add the natural arrows between these new objects (e.g. the kernel of $f$ maps into the kernel of $g\circ f$).  Iterate this process until it terminates (which it does, as there are finitely many arrows, and thus only finitely many subquotients of objects they induce).
2)  In this new diagram, tabulate all exact paths.  (This step seems to me to have high time and space complexity, unfortunately.) By exact path, I mean an infinite long exact sequence, for which all but finitely many objects are zero.
3)  Given an exact path $$0\to A_1\to \cdots \to A_i\to \cdots \to A_n\to 0$$ write the equation $$\sum_{i=1}^n (-1)^i \dim~ A_i=0.$$
4)  Solve the resulting linear system for the $\dim~ A_i$'s.
Since we've added kernels and cokernels, solving the system tells us about injectivity and surjectivity of all the arrows.  Furthermore, as far as I can tell any (non-negative) solution to this linear system is realizable as a diagram, so this algorithm gives us any information we could get by diagram chasing.

Greg has given a good summary of this method in his answer below--he takes me to task about my assertion that any non-negative integer solution to this linear system is realizable, so I will sketch an argument (again requiring the diagram to be finite acyclic).  We also assume the diagram is "complete" in the sense that step 1) has been completed.
Partially order the objects in the diagram by saying $A\leq B$ iff $A$ is a subquotient of $B$; inductively, this is the same as saying that $B\leq B$ and $A\leq B$ if there exists $C\leq B$ such that $A$ injects into $C$ or $C$ surjects onto $A$ in this diagram.  We identify isomorphic objects; this is a poset by acyclicity.  We proceed by induction on the number of objects in the diagram.  The one-object diagram is easy, so we do the induction step.
By finiteness the diagram contains a longest chain; choose such a chain and consider its minimal element $X$.  All maps into or out of $X$ are surjections or injections, respectively, so split $X$ off of every object that maps onto it or that it maps into as a direct summand.  The diagram with $X$ removed gives the induction step.
A: This answer is a response to Daniel Litt's answer above.  First, let me distill his point.  Given a diagram of finite-dimensional vector spaces, every term $A$ has a dimension which is a non-negative integer.  In addition, every morphism $f:A \to B$ has a non-negative rank which is at most $\min(\dim A,\dim B)$.  If a pair of morphisms
$$A \stackrel{f}{\longrightarrow} B \stackrel{g}{\longrightarrow} C,$$
then you get a linear relation
$$\mathrm{rank}\ f + \mathrm{rank}\ g = \dim B.$$
Thus, there is an integer programming problem to express whether the dimensions and ranks are feasible.  Since such an integer programming problem is homogeneous, you can instead treat it as a rational linear programming problem and later clear denominators.  There is an algorithm to determine feasibility, even a polynomial time algorithm.  As Daniel points out, this is enough to establish the nine lemma in the special case of finite-dimensional vector spaces.  The argument/algorithm even works in many categories other than finite-dimensional vector spaces.  For instance it works for finite abelian groups.  On the other hand, the algorithm doesn't use the fact that any polygons in the diagram commute (see below), other than perhaps a preprocessing stage in which commutative polygons are filled in by commutative triangles.
Like me, Daniel asked to restrict to acyclic diagrams.  However, I realized that this restriction is ineffectual for my entire question.  (Thus, his algorithm can't need it.)  You can convert any diagram into an acyclic one using the fact that
$$0 \longrightarrow A \stackrel{\phi}{\longrightarrow} A' \longrightarrow 0$$
makes $\phi$ into an isomorphism.  If $\mathcal{D}$ is a diagram, you should first triangulate all commutative polygons in to make commutative triangles.  Then make three copies $A, A', A''$ of each object $A \in \mathcal{D}$ together with isomorphisms
$$A \stackrel{\phi}{\longrightarrow} A' \stackrel{\phi'}{\longrightarrow} A'.$$
Then a homomorphism $f:A \to B$ in $\mathcal{D}$ can be expressed acyclically as this commutative square:
$$\begin{matrix} A & \stackrel{f}{\longrightarrow} & B' \\
\downarrow && \downarrow \\
A' & \stackrel{f'}{\longrightarrow} & B'' \end{matrix}$$
Finally, a commutative triangle $h = f \circ g$ can be expressed as a commutative square $h' \circ \phi = f' \circ g$.  Or if $f$ and $g$ are an exact pair, you can require that $f'$ and $g$ make an exact pair.
Daniel also says without explanation that if there is a solution to the dimension and rank equations, then there are ways to fill in all of the maps.  But without a lot more work, I don't think that this inference is reasonable.  The hard part is satisfying commutative triangles.  It is certainly not true that there is simply a canonical choice for each map using a skeleton $\{k^n\}$ of the category of finite-dimensional vector spaces.  Because, if $f$ and $g$ each have some rank, then their composition $f \circ g$ might also have some desired rank, and that rank depends on the choices of $f$ and $g$.  One interesting remark here is that
$$\mathrm{rank}\ f \circ g \le \min(\mathrm{rank}\ f,\mathrm{rank}\ g),$$
and there is a similar inequality on the other side.  However, I think that there is more going on than that.
Finally, it is worth giving a simple example to show that feasibility in finite-dimensional vector spaces is not the same as feasibility in vector spaces.  Given the exact sequence
$$0 \longrightarrow A \longrightarrow A \longrightarrow A \longrightarrow 0,$$
you can conclude (using the dimension equations that Daniel suggests) that $A = 0$ if it is finite-dimensional.  But if it is infinite-dimensional, then there are non-trivial solutions.
A: I'm not sure this is what you are looking for, but if you look at Gelfand and Manin's Methods of Homological Algebra, the end of Section II.5, they make the following definition:
Let $Y$ be an object of an abelian category. An element of $Y$ is a pair $(X,h)$, with $h: X \to Y$, modulo the equivalence relation that $(X,h) \sim (X',h')$ if we can complete the square
$$\begin{matrix} Z & \to & X' \\ \downarrow & & \downarrow \\ X & \to & Y \end{matrix}$$
so that the maps $Z \to X$ and $Z \to X'$ are surjective.
The map sending an object $Y$ to its elements, $E(Y)$, is clearly a functor from our Abelian category to PointedSetsWithAnInvolution, where the labelled point of $E(Y)$ is the zero map $0 \to Y$ and the involution is $(X,h) \mapsto (X,-h)$.  (It seems to me that $(X,h)$ and $(X,-h)$ are always equivalent, but G+M sometimes use notation which seems to distinguish the elements $e$ and $-e$, so I am following them.) Gelfand and Manin state as exercises:


*

*A map $f: Y_1 \to Y_2$ is a monomorphism iff $E(f)^{-1}(0) =0$ iff $E(f)$ is injective.

*A map $f: Y_1 \to Y_2$ is a epimorphism iff $E(f)$ is surjective.

*A map $f: Y_1 \to Y_2$ is zero iff $E(f)$ is zero.

*A sequence $Y_1 \to Y_2 \to Y_3$ is exact iff, for $e \in E(Y_2)$, the element $e$ is taken to the element $0 \in E(Y_3)$ if and only if it is in the image of $E(Y_1)$.

*If $y_1$ and $y_2 \in E(Y)$ then there is an element $z \in E(Y)$ such that, for any $f: Y \to Y'$ with $f(y_i)=0$, we have $f(z)=(-1)^i f(y_{1-i})$. Moreover, if $g: Y \to X$ is any map such that $g(y_1) = g(y_{2})$, we can take $z$ such that $g(z)=0$. (So $z$ acts like $y-y'$. Note that there is not claimed to be a unique $z$ which works.)


G and M then give several examples to demonstrate that most diagram chasing arguments can be rewrittten using the $E$ construction.
A: This was originally going to be a rather different post, but I realized that my argument could perhaps be adapted into an (ineffective) algorithm, if it's possible to patch up the hole. At the very least, I should say some things which might be obvious but wasn't to me until I saw it, and so might not be obvious to someone else either.
Let's fix the abelian category to be the category of finite-dimensional vector spaces over GF(2). We have a decorated diagram of the type Greg describes. Then it's easy to see that the non-exactness of two composable arrows is in RE -- we can have a prover just give us a counterexample, and since everything's finite-dimensional, we're good. So the "diagram chasing decision problem" is in coRE.
If we could effectively bound the dimensions of the vector spaces in a counterexample, of course, we'd have that the problem was recursive. At least for finite-dimensional vector spaces over a finite field. But I don't know how this is possible. My question, though: is it possible to get around the need for an effective bound somehow? I think you can get a complexity-theoretic improvement by letting the prover compute everything as a black box and "checking for honesty" on logarithmic-sized subspaces, but I might be misremembering. Is there some extraordinarily clever way to do something like this for computability? (I'm thinking about results like the necklace reconstruction problem, or problem B6 on this year's Putnam exam, although in both of those cases the "uniform bound" hides a lot of information that doesn't seem to have anyplace to go in this scenario...)
Actually, I guess really the only scenario to worry about would be if the dimensions in the smallest counterexample to exactness of some pair grew faster than any computable function of the size of the diagram, right? Otherwise we have that the problem is in co-NSPACE(BigFunction(n)), and so it's in NSPACE(BigFunction(n)). That kind of growth rate seems implausible, but again I have no idea how to prove it's impossible.
A: This is an old question, but I think I have a reasonably complete solution to this problem.  It gives you a criterion for when you can answer a question by a diagram chase, and a procedure for actually doing it.  I will sketch the answer here, and if anyone is still interested in this question, I will make a more formal write-up.
Diagram chase arguments make sense for pointed sets, which I will think of as vector spaces over $F_1$ (the field of one element).  Maps between pointed sets are required to have well-defined kernels and cokernels, i.e. they are partial bijections for nonzero elements.  In this setting, diagram chases are even simpler because when you chase an element backward or forward, there's only one possibility.
So what good does this do us?  It turns out that when the diagram is simple enough,
theorems over $F_1$ can be lifted to arbitrary abelian categories.  I will call these diagrams “chaseable”.  You can associate with each object in the diagram the lattice of subobjects containing the zero object, the whole object, and closed under taking images and inverse images.  If that lattice is finite and distributive for each object, then the diagram is chaseable.  The main reason it would fail to be finite is if the diagram has loops.  It is easy to find cases where it fails to be distributive (the $D_3$ quiver is a ready example), but double complexes give you lattices that are both finite and distributive.  (To me this ``explains'' the prominence of double complexes -- they are much simpler than arbitrary diagrams.)
Once you associate a finite distributive lattice to each object, you can use the Birkhoff representation theorem to understand the lattice.  You can associate to each join-irreducible element a one-element generator of a $F_1$-vector space.  If you follow that element around, you get an indecomposable representation of the diagram over $F_1$.  If a condition such as being exact holds for indecomposable $F_1$ representations, then it holds for the diagram.
This is sufficient to prove results such as the five or nine lemmas.  Results that imply the existence of maps, such as the snake lemma or the connecting homomorphism for long exact sequences require slightly more work -- the join-irreducible elements have an order, and you need to keep track of the order -- but it is doable.
You can also use the same technique to reprove the characterization of finite-dimensional indecomposable modules over string algebras -- the indecomposable representations over a field correspond to the indecomposable representations over $F_1$.
