Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-15 08:16 cc47aff4

View on Github →

feat(algebra/homology): truncation and augmentation of chain complexes (#7480)

Estimated changes

Created src/algebra/homology/augment.lean

added def chain_complex.augment

added theorem chain_complex.augment_X_succ

added theorem chain_complex.augment_X_zero

added theorem chain_complex.augment_d_one_zero

added theorem chain_complex.augment_d_succ_succ

added def chain_complex.augment_truncate

added theorem chain_complex.augment_truncate_hom_f_succ

added theorem chain_complex.augment_truncate_hom_f_zero

added theorem chain_complex.augment_truncate_inv_f_succ

added theorem chain_complex.augment_truncate_inv_f_zero

added theorem chain_complex.cochain_complex_d_succ_succ_zero

added def chain_complex.to_single₀_as_complex

added def chain_complex.truncate

added def chain_complex.truncate_augment

added theorem chain_complex.truncate_augment_hom_f

added theorem chain_complex.truncate_augment_inv_f

added def chain_complex.truncate_to