Commit 2023-11-10 20:41 ecdd87a3
View on Github →refactor(Algebra/Homology): remove single₀ (#8208)
This PR removes the special definitions of single₀
for chain and cochain complexes, so as to avoid duplication of code with HomologicalComplex.single
which is the functor constructing the complex that is supported by a single arbitrary degree. single₀
was supposed to have better definitional properties, but it turns out that in Lean4, it is no longer true (at least for the action of this functor on objects). The computation of the homology of these single complexes is generalized for HomologicalComplex.single
using the new homology API: this result is moved to a separate file Algebra.Homology.SingleHomology
.