Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-05-20 02:00
641cece5
View on Github →
feat(algebra/homology): the homotopy category (
#7484
)
Estimated changes
Created
src/algebra/homology/homotopy_category.lean
added
def
category_theory.functor.map_homotopy_category
added
def
category_theory.nat_trans.map_homotopy_category
added
theorem
category_theory.nat_trans.map_homotopy_category_comp
added
theorem
category_theory.nat_trans.map_homotopy_category_id
added
def
homotopic
added
theorem
homotopy_category.eq_of_homotopy
added
def
homotopy_category.homology_factors
added
theorem
homotopy_category.homology_factors_hom_app
added
theorem
homotopy_category.homology_factors_inv_app
added
def
homotopy_category.homology_functor
added
theorem
homotopy_category.homology_functor_map_factors
added
def
homotopy_category.homotopy_equiv_of_iso
added
def
homotopy_category.homotopy_of_eq
added
def
homotopy_category.homotopy_out_map
added
def
homotopy_category.iso_of_homotopy_equiv
added
def
homotopy_category.quotient
added
theorem
homotopy_category.quotient_map_out
added
theorem
homotopy_category.quotient_map_out_comp_out
added
theorem
homotopy_category.quotient_obj_as
added
def
homotopy_category