Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-15 08:16 c63caebb

View on Github →

feat(algebra/homology): homotopies between chain maps (#7483)

Estimated changes

Modified src/algebra/homology/additive.lean

Created src/algebra/homology/homotopy.lean

added def category_theory.functor.map_homotopy

added def category_theory.functor.map_homotopy_equiv

added def from_next'

added theorem from_next'_add

added theorem from_next'_comp_left

added theorem from_next'_comp_right

added theorem from_next'_eq

added theorem from_next'_neg

added theorem from_next'_zero

added theorem homology_map_eq_of_homotopy

added def homology_obj_iso_of_homotopy_equiv

added theorem homotopy.comm

added def homotopy.comp_left

added def homotopy.comp_left_id

added def homotopy.comp_right

added def homotopy.comp_right_id

added def homotopy.equiv_sub_zero

added theorem homotopy.from_next'_succ_chain_complex

added theorem homotopy.from_next'_zero_chain_complex

added def homotopy.from_next

added def homotopy.mk_inductive

added def homotopy.mk_inductive_aux₁

added def homotopy.mk_inductive_aux₂

added theorem homotopy.mk_inductive_aux₃

added def homotopy.refl

added def homotopy.symm

added theorem homotopy.to_prev'_chain_complex

added def homotopy.to_prev

added def homotopy.trans

added structure homotopy

added def homotopy_equiv.refl

added def homotopy_equiv.symm

added def homotopy_equiv.trans

added structure homotopy_equiv

added def to_prev'

added theorem to_prev'_add

added theorem to_prev'_comp_left

added theorem to_prev'_comp_right

added theorem to_prev'_eq

added theorem to_prev'_neg

added theorem to_prev'_zero