Commit 2024-07-15 21:28 f9724359

View on Github →

feat: the abelian group structure on Ext-groups in abelian categories (#14496) In this PR, we construct the abelian group structure on Ext-groups.

Estimated changes

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

added theorem CategoryTheory.Abelian.Ext.add_comp

added theorem CategoryTheory.Abelian.Ext.add_hom

added theorem CategoryTheory.Abelian.Ext.biprod_ext

added theorem CategoryTheory.Abelian.Ext.comp_add

added theorem CategoryTheory.Abelian.Ext.comp_mk₀_id

added theorem CategoryTheory.Abelian.Ext.comp_neg

added theorem CategoryTheory.Abelian.Ext.comp_zero

added theorem CategoryTheory.Abelian.Ext.ext_iff

added theorem CategoryTheory.Abelian.Ext.homAddEquiv_apply

added theorem CategoryTheory.Abelian.Ext.mk₀_comp_mk₀

added theorem CategoryTheory.Abelian.Ext.mk₀_comp_mk₀_assoc

added theorem CategoryTheory.Abelian.Ext.mk₀_hom

added theorem CategoryTheory.Abelian.Ext.mk₀_id_comp

added theorem CategoryTheory.Abelian.Ext.mk₀_zero

added theorem CategoryTheory.Abelian.Ext.neg_comp

added theorem CategoryTheory.Abelian.Ext.neg_hom

added theorem CategoryTheory.Abelian.Ext.zero_comp

added theorem CategoryTheory.Abelian.Ext.zero_hom

Modified Mathlib/CategoryTheory/Localization/SmallShiftedHom.lean

added theorem CategoryTheory.Localization.SmallShiftedHom.equiv_mk₀

Modified Mathlib/CategoryTheory/Shift/ShiftedHom.lean

added theorem CategoryTheory.ShiftedHom.comp_neg

added theorem CategoryTheory.ShiftedHom.mk₀_comp_mk₀

added theorem CategoryTheory.ShiftedHom.mk₀_comp_mk₀_assoc

added theorem CategoryTheory.ShiftedHom.mk₀_zero

added theorem CategoryTheory.ShiftedHom.neg_comp