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