Commit 2026-01-05 14:32 76689c2a

View on Github →

feat(Homology): map between Ext induced by exact functor (#31707) In this PR, we developed the additive map Ext(M,N) => Ext(F(M), F(N)) when F is exact functor between abelian category. We also developed its linear version when F is linear.

Estimated changes

Modified Mathlib.lean

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

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

added theorem CategoryTheory.Abelian.Ext.mapExactFunctor_add

added theorem CategoryTheory.Abelian.Ext.mapExactFunctor_hom

added theorem CategoryTheory.Abelian.Ext.mapExactFunctor_zero

added theorem CategoryTheory.Functor.mapExactFunctor_smul

added theorem CategoryTheory.Functor.mapExtAddHom_apply

added theorem CategoryTheory.Functor.mapExtAddHom_coe

added theorem CategoryTheory.Functor.mapExtLinearMap_apply

added theorem CategoryTheory.Functor.mapExtLinearMap_coe

added theorem CategoryTheory.Functor.mapExtLinearMap_toAddMonoidHom

Modified Mathlib/Algebra/Homology/HomotopyCategory.lean

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

Modified Mathlib/CategoryTheory/Linear/LinearFunctor.lean

added theorem CategoryTheory.Functor.linear_comp_iff_of_full_of_essSurj

added theorem CategoryTheory.Functor.linear_of_full_essSurj_comp

Modified Mathlib/CategoryTheory/Shift/CommShift.lean

Modified Mathlib/CategoryTheory/Shift/ShiftedHom.lean