Commit 2023-12-27 10:11 d412c821

feat(Algebra/Homology): computation of the connecting homomorphism of the homology sequence (#8771) This PR adds a variant of a lemma introduced in #8512: ShortComplex.SnakeInput.δ_apply' computes the connecting homomorphism of the snake lemma in a concrete categoriy C with a phrasing based on the functor forget₂ C Ab rather than forget C. From this, the lemma ShortComplex.ShortExact.δ_apply is obtained in a new file Algebra.Homology.ConcreteCategory: it gives a computation in terms of (co)cycles of the connecting homomorphism in homology attached to a short exact sequence of homological complexes in C. This PR also adds a lemma which computes "up to refinements" the connecting homomorphism of the homology sequence in general abelian categories.