Commit 2024-08-23 14:42 c3785527

View on Github →

feat(Algebra/Homology): the Ext class of a short exact sequence (#14793) In this PR, we construct the class in Ext S.X₃ S.X₁ 1 that is attached to a short exact short complex S in an abelian category.

Estimated changes

Modified Mathlib.lean

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

added theorem DerivedCategory.singleFunctorsPostcompQIso_hom_hom

added theorem DerivedCategory.singleFunctorsPostcompQIso_inv_hom

Renamed Mathlib/Algebra/Homology/DerivedCategory/Ext.lean to Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean

added theorem CategoryTheory.Abelian.Ext.comp_assoc_of_second_deg_zero

added theorem CategoryTheory.Abelian.Ext.comp_assoc_of_third_deg_zero

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

added theorem CategoryTheory.ShortComplex.ShortExact.comp_extClass

added theorem CategoryTheory.ShortComplex.ShortExact.extClass_comp

added theorem CategoryTheory.ShortComplex.ShortExact.extClass_hom

Modified Mathlib/CategoryTheory/Localization/SmallHom.lean

added theorem CategoryTheory.Localization.hasSmallLocalizedHom_iff_source

added theorem CategoryTheory.Localization.hasSmallLocalizedHom_iff_target

Modified Mathlib/CategoryTheory/Localization/SmallShiftedHom.lean

added theorem CategoryTheory.Localization.hasSmallLocalizedShiftedHom_iff_source

added theorem CategoryTheory.Localization.hasSmallLocalizedShiftedHom_iff_target

Modified Mathlib/CategoryTheory/Shift/Localization.lean

added theorem CategoryTheory.MorphismProperty.shift

Modified Mathlib/CategoryTheory/Sites/SheafCohomology/Basic.lean

Modified Mathlib/CategoryTheory/Triangulated/Yoneda.lean