feat(algebra/homology): chain complexes (#2174)
* thoughts on chain complexes
* minor
* feat(category_theory): split epis and monos, and a result about (co)projections
* total functor faithful
* homology!
* remove lint
* something something homology
* comment out broken stuff
* adding comments
* various
* rewrite
* fixes
* Update src/category_theory/epi_mono.lean
* Update src/category_theory/epi_mono.lean
* Update src/category_theory/epi_mono.lean
* better use of ext
* feat(category_theory): subsingleton (has_zero_morphisms)
* revert some independent changes moved to #2180
* revert some independent changes moved to #2181
* revert independent changes moved to #2182
* fix
* Apply suggestions from code review
Co-Authored-By: Johan Commelin <johan@commelin.net>
* changes from review
* module docs
* various
* Update src/category_theory/shift.lean
Co-Authored-By: Kevin Buzzard <k.buzzard@imperial.ac.uk>
* various
* various fixes
* fix
* all the minor suggestions
Co-Authored-By: Markus Himmel <markus@himmel-villmar.de>
* ugh... fix reverting stuff from #2180
* off by one
* various
* use abbreviation
* chain as well as cochain
* satisfy the linter
* some simp lemmas
* simp lemmas
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
