Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-04 15:53 e7161393

View on Github →

feat(algebra/homology/Module): API for complexes of modules (#12622) API for homological complexes in Module R.

Estimated changes

Modified src/algebra/category/Module/kernels.lean

added theorem Module.cokernel_π_ext

Modified src/algebra/category/Module/subobject.lean

added theorem Module.cokernel_π_image_subobject_ext

added theorem Module.to_kernel_subobject_arrow

Created src/algebra/homology/Module.lean

added theorem Module.cycles_ext

added theorem Module.cycles_map_to_cycles

added theorem Module.homology_ext'

added theorem Module.homology_ext

added def Module.to_cycles

added def Module.to_homology

Modified src/algebra/homology/homology.lean

modified theorem cycles_map_arrow

deleted theorem homological_complex.boundaries_to_cycles_arrow

modified def homological_complex.cycles

deleted theorem homological_complex.cycles_arrow_d_from

Modified src/category_theory/limits/concrete_category.lean

added theorem category_theory.limits.cokernel_funext