Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-26 00:32 6e6c81a4

View on Github →

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

Estimated changes