Commit 2023-04-24 05:58 c6ead01f

View on Github →

feat: port Algebra.Homology.HomotopyCategory (#3602)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/HomotopyCategory.lean

added def CategoryTheory.Functor.mapHomotopyCategory

added theorem CategoryTheory.Functor.mapHomotopyCategory_map

added def CategoryTheory.NatTrans.mapHomotopyCategory

added theorem CategoryTheory.NatTrans.mapHomotopyCategory_comp

added theorem CategoryTheory.NatTrans.mapHomotopyCategory_id

added theorem HomotopyCategory.eq_of_homotopy

added def HomotopyCategory.homologyFactors

added theorem HomotopyCategory.homologyFactors_hom_app

added theorem HomotopyCategory.homologyFactors_inv_app

added def HomotopyCategory.homologyFunctor

added theorem HomotopyCategory.homologyFunctor_map_factors

added def HomotopyCategory.homotopyEquivOfIso

added def HomotopyCategory.homotopyOfEq

added def HomotopyCategory.homotopyOutMap

added def HomotopyCategory.isoOfHomotopyEquiv

added theorem HomotopyCategory.quot_mk_eq_quotient_map

added def HomotopyCategory.quotient

added theorem HomotopyCategory.quotient_map_out

added theorem HomotopyCategory.quotient_map_out_comp_out

added theorem HomotopyCategory.quotient_obj_as

added def HomotopyCategory

added def homotopic