Commit 2023-11-24 13:15 9988ed68

View on Github →

feat: limits and colimits in the category of homological complexes (#8472)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/HomologicalComplexLimits.lean

added def HomologicalComplex.isColimitOfEval

added def HomologicalComplex.isLimitOfEval

added def HomologicalComplex.preservesColimitsOfShapeOfEval

added def HomologicalComplex.preservesLimitsOfShapeOfEval