Commit 2023-11-28 07:37 d835056c
View on Github →feat: computation of the connecting homomorphism of the snake lemma in concrete categories (#8512)
This PR provides a lemma ShortComplex.SnakeInput.δ_apply which allows the computation of the connecting homomorphism in concrete categories. Incidentally, we also deduce from previous results that functors which preserve homology preserve finite limits and finite colimits.