Commit 2025-10-29 00:03 53655df9

View on Github →

feat(Algebra/Homology): Ext modules (#27416) In this PR, we show that if C is a R-linear abelian category, then there is a R-module structure on the groups Ext X Y n for X and Y in C and n : ℕ.

Estimated changes

Modified Mathlib.lean

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

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

added theorem CategoryTheory.Abelian.Ext.comp_smul

added theorem CategoryTheory.Abelian.Ext.mk₀_linearEquiv₀_apply

added theorem CategoryTheory.Abelian.Ext.mk₀_smul

added theorem CategoryTheory.Abelian.Ext.smul_comp

added theorem CategoryTheory.Abelian.Ext.smul_eq_comp_mk₀

added theorem CategoryTheory.Abelian.Ext.smul_hom

Modified Mathlib/Algebra/Homology/DerivedCategory/Linear.lean

Modified Mathlib/CategoryTheory/Shift/ShiftedHom.lean

added theorem CategoryTheory.ShiftedHom.comp_smul

added theorem CategoryTheory.ShiftedHom.mk₀_smul

added theorem CategoryTheory.ShiftedHom.smul_comp