Commit 2023-09-18 15:32 0d6cb15f

View on Github →

feat: functors which preserve homology (#7197)

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.Functor.PreservesHomology.preservesCokernel

added def CategoryTheory.Functor.PreservesHomology.preservesKernel

added def CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hf'

added def CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hg

added theorem CategoryTheory.ShortComplex.LeftHomologyData.map_f'

added def CategoryTheory.ShortComplex.LeftHomologyMapData.map