Take the tour ×  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