Commit 2026-01-16 21:23 9989fd28

View on Github →

feat(Algebra/Homology): functoriality of extMk with respect to the injective resolution (#33360) The dual statement for projective resolutions is also obtained.

Estimated changes

Modified Mathlib/Algebra/Homology/HomotopyCategory/HomComplexSingle.lean

added theorem CochainComplex.HomComplex.Cochain.fromSingleMk_postcomp

added theorem CochainComplex.HomComplex.Cochain.toSingleMk_precomp

added theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_postcomp

added theorem CochainComplex.HomComplex.Cocycle.toSingleMk_precomp

Modified Mathlib/CategoryTheory/Abelian/Injective/Ext.lean

added theorem CategoryTheory.InjectiveResolution.extMk_comp_mk₀

added theorem CategoryTheory.InjectiveResolution.extMk_hom

Modified Mathlib/CategoryTheory/Abelian/Injective/Extend.lean

added theorem CategoryTheory.InjectiveResolution.Hom.hom'_f

added theorem CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom'

Modified Mathlib/CategoryTheory/Abelian/Projective/Ext.lean

added theorem CategoryTheory.ProjectiveResolution.extMk_hom

added theorem CategoryTheory.ProjectiveResolution.mk₀_comp_extMk

Modified Mathlib/CategoryTheory/Abelian/Projective/Extend.lean

added theorem CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π'

added theorem CategoryTheory.ProjectiveResolution.Hom.hom'_f

Modified Mathlib/CategoryTheory/Preadditive/Injective/Resolution.lean

added theorem CategoryTheory.InjectiveResolution.Hom.ι_comp_hom

added structure CategoryTheory.InjectiveResolution.Hom

Modified Mathlib/CategoryTheory/Preadditive/Projective/Resolution.lean

added theorem CategoryTheory.ProjectiveResolution.Hom.hom_comp_π

added structure CategoryTheory.ProjectiveResolution.Hom