Commit 2024-04-16 07:45 f47773f1

View on Github →

feat(Algebra/Homology): relax assumptions for Functor.mapHomologicalComplex (#12174) The extension of a functor F to a functor between categories of homological complex is now defined under the assumption F.PreservesZeroMorphisms rather than F.Additive.

Estimated changes

Modified Mathlib/Algebra/Homology/Additive.lean

modified def CategoryTheory.Equivalence.mapHomologicalComplex

modified def CategoryTheory.Functor.mapHomologicalComplex

modified def CategoryTheory.NatIso.mapHomologicalComplex

modified def CategoryTheory.NatTrans.mapHomologicalComplex

modified theorem CategoryTheory.NatTrans.mapHomologicalComplex_comp

modified theorem CategoryTheory.NatTrans.mapHomologicalComplex_id

modified theorem CategoryTheory.NatTrans.mapHomologicalComplex_naturality

modified theorem ChainComplex.map_chain_complex_of

modified theorem HomologicalComplex.singleMapHomologicalComplex_hom_app_ne

modified theorem HomologicalComplex.singleMapHomologicalComplex_hom_app_self

modified theorem HomologicalComplex.singleMapHomologicalComplex_inv_app_ne

modified theorem HomologicalComplex.singleMapHomologicalComplex_inv_app_self