Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-05-14 17:28
a52f471f
View on Github →
feat(algebra/homology): chain complexes are an additive category (
#7478
)
Estimated changes
Created
src/algebra/homology/additive.lean
added
def
category_theory.functor.map_homological_complex
added
def
category_theory.nat_trans.map_homological_complex
added
theorem
category_theory.nat_trans.map_homological_complex_comp
added
theorem
category_theory.nat_trans.map_homological_complex_id
added
theorem
category_theory.nat_trans.map_homological_complex_naturality
added
def
chain_complex.single₀_map_homological_complex
added
theorem
chain_complex.single₀_map_homological_complex_hom_app_succ
added
theorem
chain_complex.single₀_map_homological_complex_hom_app_zero
added
theorem
chain_complex.single₀_map_homological_complex_inv_app_succ
added
theorem
chain_complex.single₀_map_homological_complex_inv_app_zero
added
theorem
homological_complex.add_f_apply
added
theorem
homological_complex.neg_f_apply
added
def
homological_complex.single_map_homological_complex
added
theorem
homological_complex.single_map_homological_complex_hom_app_ne
added
theorem
homological_complex.single_map_homological_complex_hom_app_self
added
theorem
homological_complex.single_map_homological_complex_inv_app_ne
added
theorem
homological_complex.single_map_homological_complex_inv_app_self
added
theorem
homological_complex.sub_f_apply
added
theorem
homological_complex.zero_f_apply
Modified
src/algebra/homology/single.lean