Commit 2023-09-08 11:01 338f41e0

View on Github →

feat: definition of the homology of a short complex (#6994) This PR introduces the definition S.homology for a short complex S that "has homology".

Estimated changes

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

added theorem CategoryTheory.ShortComplex.HasHomology.mk'

added def CategoryTheory.ShortComplex.HomologyMapData.comp

added def CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork

added def CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsLimitKernelFork

added def CategoryTheory.ShortComplex.HomologyMapData.id

added def CategoryTheory.ShortComplex.HomologyMapData.ofIsColimitCokernelCofork

added def CategoryTheory.ShortComplex.HomologyMapData.ofIsLimitKernelFork

added def CategoryTheory.ShortComplex.HomologyMapData.ofZeros

added def CategoryTheory.ShortComplex.HomologyMapData.op

added def CategoryTheory.ShortComplex.HomologyMapData.unop

added def CategoryTheory.ShortComplex.HomologyMapData.zero

added theorem CategoryTheory.ShortComplex.hasHomology_of_epi_of_isIso_of_mono'

added theorem CategoryTheory.ShortComplex.hasHomology_of_epi_of_isIso_of_mono

added theorem CategoryTheory.ShortComplex.hasHomology_of_iso

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

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