Commit 2023-10-11 07:51 451325f4

View on Github →

feat: functors which preserves right homology (#7256)

Estimated changes

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

added def CategoryTheory.Functor.PreservesLeftHomologyOf.mk'

added def CategoryTheory.Functor.PreservesRightHomologyOf.mk'

added def CategoryTheory.ShortComplex.HomologyMapData.map

added def CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hf

added def CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hg'

added theorem CategoryTheory.ShortComplex.RightHomologyData.map_g'

added def CategoryTheory.ShortComplex.RightHomologyMapData.map