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.

4more comments