Commit 2020-04-13 08:52 92c8d93d

feat(algebra/homology): the cohomology functor (#2374) This is the second in a series of most likely three PRs about the cohomology functor. As such, this PR depends on #2373. In the project laid out in homology.lean, @semorrison asks what the minimal assumptions are that are needed to get induced maps on images. In this PR, I offer a tautologial answer to this question: We get induced maps on images when there are induced maps on images. In this way, we can let type class resolution answer the question whether cohomology is functorial. In particular, the third PR will contain the fact that if our images are strong epi-mono factorizations, then we get induced maps on images. Since the regular coimage construction in regular categories is a strong epi-mono factorization, the approach in this PR generalizes the previous suggestion of requiring V to be regular. A quick remark about cohomology and dependent types: As you can see, at one point Lean forces us to write i - 1 + 1 instead of i because these two things are not definitionally equal. I am afraid, as we do more with cohomology, there will be many cases of this issue, and to compose morphisms whose types contain different incarnations of the same integer, we will have to insert some eq_to_hom-esque glue and pray that we will be able to rewrite them all away in the proofs without getting the beloved motive is not type correct error. Maybe there is some better way to solve this problem? (Or am I overthinking this and it is not actually going to be an issue at all?)