Commit 2023-05-25 13:40 f4520b46

View on Github →

feat: port CategoryTheory.Abelian.InjectiveResolution (#4059)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean

added def CategoryTheory.InjectiveResolution.desc

added def CategoryTheory.InjectiveResolution.descCompHomotopy

added def CategoryTheory.InjectiveResolution.descFOne

added theorem CategoryTheory.InjectiveResolution.descFOne_zero_comm

added def CategoryTheory.InjectiveResolution.descFSucc

added def CategoryTheory.InjectiveResolution.descFZero

added def CategoryTheory.InjectiveResolution.descHomotopy

added def CategoryTheory.InjectiveResolution.descHomotopyZero

added def CategoryTheory.InjectiveResolution.descHomotopyZeroOne

added def CategoryTheory.InjectiveResolution.descHomotopyZeroSucc

added def CategoryTheory.InjectiveResolution.descHomotopyZeroZero

added def CategoryTheory.InjectiveResolution.descIdHomotopy

added theorem CategoryTheory.InjectiveResolution.desc_commutes

added theorem CategoryTheory.InjectiveResolution.exact_ofCocomplex

added def CategoryTheory.InjectiveResolution.homotopyEquiv

added theorem CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι

added theorem CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι

added def CategoryTheory.InjectiveResolution.ofCocomplex

added theorem CategoryTheory.InjectiveResolution.ofCocomplex_sq_01_comm

added theorem CategoryTheory.exact_f_d

added def CategoryTheory.injectiveResolutions

added def HomologicalComplex.Hom.HomologicalComplex.Hom.fromSingle₀InjectiveResolution