Commit 2024-06-25 06:18 7bdafea9

View on Github →

feat(Algebra/Homology) the single complex functor preserves (co)limits (#13875) In this PR, it is shown that the single functors C ⥤ HomologicalComplex C c preserves limits and colimits.

Estimated changes

Modified Mathlib/Algebra/Homology/HomologicalComplexLimits.lean

Modified Mathlib/Algebra/Homology/Single.lean

added theorem HomologicalComplex.isZero_single_comp_eval

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean

added def CategoryTheory.Functor.preservesColimitsOfShapeOfIsZero

added def CategoryTheory.Functor.preservesColimitsOfSizeOfIsZero

added def CategoryTheory.Functor.preservesLimitsOfShapeOfIsZero

added def CategoryTheory.Functor.preservesLimitsOfSizeOfIsZero

Modified Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean

added theorem CategoryTheory.Limits.IsColimit.isZero_pt

added def CategoryTheory.Limits.IsColimit.ofIsZero

added theorem CategoryTheory.Limits.IsLimit.isZero_pt

added def CategoryTheory.Limits.IsLimit.ofIsZero