Commit 2023-10-12 10:52 238b4602

View on Github →

feat: naturality of the isomorphisms induced by functors which preserves homology (#7624) If F : C ⥤ D is a functor which preserves homlogy (e.g. preserves finite limits/colimits), there is a natural isomorphism F.mapShortComplex ⋙ ShortComplex.homologyFunctor D ≅ ShortComplex.homologyFunctor C ⋙ F which expresses that F "commutes" with homology.

Estimated changes

Modified Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean

added def CategoryTheory.ShortComplex.HomologyMapData.natTransApp

added def CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp

added def CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp

added theorem CategoryTheory.ShortComplex.homologyMap_mapNatTrans

added theorem CategoryTheory.ShortComplex.mapHomologyIso'_eq_mapHomologyIso

added theorem CategoryTheory.ShortComplex.mapHomologyIso'_hom_naturality

added theorem CategoryTheory.ShortComplex.mapHomologyIso'_inv_naturality

added theorem CategoryTheory.ShortComplex.mapHomologyIso_hom_naturality

added theorem CategoryTheory.ShortComplex.mapHomologyIso_inv_naturality

added theorem CategoryTheory.ShortComplex.mapOpcyclesIso_hom_naturality

added theorem CategoryTheory.ShortComplex.mapOpcyclesIso_inv_naturality

added theorem CategoryTheory.ShortComplex.mapRightHomologyIso_hom_naturality

added theorem CategoryTheory.ShortComplex.mapRightHomologyIso_inv_naturality