Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-13 15:18 ce455949

View on Github →

feat(algebra/homology/single): chain complexes supported in a single degree (#7477)

Estimated changes

Modified src/algebra/homology/homological_complex.lean

Created src/algebra/homology/single.lean

added def chain_complex.homology_functor_0_single₀

added def chain_complex.homology_functor_succ_single₀

added def chain_complex.single₀

added def chain_complex.single₀_iso_single

added theorem chain_complex.single₀_map_f_0

added theorem chain_complex.single₀_map_f_succ

added theorem chain_complex.single₀_obj_X_0

added theorem chain_complex.single₀_obj_X_d

added theorem chain_complex.single₀_obj_X_d_from

added theorem chain_complex.single₀_obj_X_d_to

added theorem chain_complex.single₀_obj_X_succ

added def chain_complex.to_single₀_equiv

added def homological_complex.single

added theorem homological_complex.single_map_f_self

added def homological_complex.single_obj_X_self

Modified src/category_theory/fully_faithful.lean

added def category_theory.full.of_iso