Commit 2023-05-01 20:06 3d2204e1

View on Github →

feat: port CategoryTheory.Preadditive.ProjectiveResolution (#3740)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Preadditive/ProjectiveResolution.lean

added theorem CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero

added theorem CategoryTheory.ProjectiveResolution.complex_d_succ_comp

added def CategoryTheory.ProjectiveResolution.homotopyEquiv

added theorem CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π

added theorem CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π

added def CategoryTheory.ProjectiveResolution.lift

added def CategoryTheory.ProjectiveResolution.liftCompHomotopy

added def CategoryTheory.ProjectiveResolution.liftHomotopy

added def CategoryTheory.ProjectiveResolution.liftHomotopyZero

added def CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne

added def CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc

added def CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero

added def CategoryTheory.ProjectiveResolution.liftIdHomotopy

added def CategoryTheory.ProjectiveResolution.liftOne

added theorem CategoryTheory.ProjectiveResolution.liftOne_zero_comm

added def CategoryTheory.ProjectiveResolution.liftSucc

added def CategoryTheory.ProjectiveResolution.liftZero

added theorem CategoryTheory.ProjectiveResolution.lift_commutes

added def CategoryTheory.ProjectiveResolution.self

added theorem CategoryTheory.ProjectiveResolution.π_f_succ

added structure CategoryTheory.ProjectiveResolution

added def CategoryTheory.projectiveResolution

added def CategoryTheory.projectiveResolutions