Mathlib Changelog
v3
Changelog
About
Github
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