Commit 2025-04-28 06:56 795cc063

View on Github →

feat(CategoryTheory/Abelian): Ext when there are enough injectives (#23797) In this PR, it is shown that Ext-groups of positive degree to an injective object vanish. It follows that if C is a w-small abelian category with enough injectives, then Ext-groups are w-small (i.e. HasExt.{w} holds). This PR dualizes the results in #19591.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean

Created Mathlib/Algebra/Homology/DerivedCategory/Ext/EnoughInjectives.lean

added theorem CategoryTheory.Abelian.Ext.eq_zero_of_injective

added theorem CategoryTheory.hasExt_of_enoughInjectives

added theorem CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective

added theorem DerivedCategory.to_singleFunctor_obj_eq_zero_of_injective

Modified Mathlib/Algebra/Homology/DerivedCategory/Ext/EnoughProjectives.lean

added theorem DerivedCategory.from_singleFunctor_obj_eq_zero_of_projective

deleted theorem DerivedCategory.from_singleFunctor_obj_projective_eq_zero

Modified Mathlib/Algebra/Homology/SingleHomology.lean

added theorem HomologicalComplex.pOpcycles_singleObjOpcyclesSelfIso_inv

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

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