Commit 2026-01-10 11:02 0c94ad3f

View on Github →

feat(Algebra/Homology): functoriality of ProjectiveResolution.extMk (#33358) Given a fixed projective (resp. injective) resolution R, we obtain the functoriality of the constructor R.extMk.

Estimated changes

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

added def CochainComplex.HomComplex.Cocycle.postcomp

added def CochainComplex.HomComplex.Cocycle.precomp

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

added theorem CochainComplex.HomComplex.Cocycle.equivHomShift_comp

added theorem CochainComplex.HomComplex.Cocycle.equivHomShift_comp_shift

added theorem CochainComplex.HomComplex.Cocycle.equivHomShift_symm_postcomp

added theorem CochainComplex.HomComplex.Cocycle.equivHomShift_symm_precomp

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

added theorem CochainComplex.HomComplex.Cochain.fromSingleEquiv_fromSingleMk

added theorem CochainComplex.HomComplex.Cochain.fromSingleMk_precomp

added theorem CochainComplex.HomComplex.Cochain.toSingleEquiv_toSingleMk

added theorem CochainComplex.HomComplex.Cochain.toSingleMk_postcomp

added theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_precomp

added theorem CochainComplex.HomComplex.Cocycle.toSingleMk_postcomp

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

added theorem CategoryTheory.InjectiveResolution.mk₀_comp_extMk

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

added theorem CategoryTheory.ProjectiveResolution.extMk_comp_mk₀