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