Commit 2023-07-31 13:14 6f17aeee

View on Github →

feat: short complexes in functor categories (#6245) This PR constructs an equivalence of categories ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean

added def CategoryTheory.ShortComplex.FunctorEquivalence.counitIso

added def CategoryTheory.ShortComplex.FunctorEquivalence.functor

added def CategoryTheory.ShortComplex.FunctorEquivalence.inverse

added def CategoryTheory.ShortComplex.FunctorEquivalence.unitIso

added def CategoryTheory.ShortComplex.functorEquivalence

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