Commit 2025-12-28 17:51 b4d4ef30
View on Github →feat(CategoryTheory): computing Ext-groups using an injective resolution (#32105)
Given an injective resolution R of an object Y in an abelian category, we define a constructor for elements in Ext X Y n which takes as input "cocycles" given as morphisms X ⟶ R.cocomplex.X n, and we provide an API for this definition.
When the dual construction for projective resolutions will be done, it may be possible to remove the old Ext API.