On free abelian categories for theorem proving

TL;DR

This paper introduces a computational method for theorem proving in homological algebra using free abelian categories, enabling explicit calculations and recovering classical results like Dowker's formula.

Contribution

It develops a computational framework based on free abelian categories for theorem proving in homological algebra, including explicit formulas and refined lemmas.

Findings

Recovered Dowker's explicit formula for the connecting homomorphism

Identified a universal sense of uniqueness for the connecting homomorphism

Provided a refined version of the 5-lemma

Abstract

We give a computational approach to theorem proving in homological algebra. This approach is based on computations in the free abelian category of an additive category $\mathbf{A}$. We show that the free abelian category is amenable to explicit computations whenever we can decide homotopy equations in $\mathbf{A}$. As some consequences of our investigations, we recover Dowker's explicit formula for the connecting homomorphism $\partial$ in the snake lemma, we find a universal sense in which $\partial$ is unique, and we give a refined version of the 5-lemma.