Commit 2023-09-18 15:32 712ddeca

View on Github →

feat: study of the left/right homology comparison morphism (#7192) In this PR, it is shown that a short complex has homology iff it has both left and right homology and that the comparison morphism between the two is an isomorphism.

Estimated changes

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

added theorem CategoryTheory.ShortComplex.exact_iff_isZero_rightHomology

deleted theorem CategoryTheory.ShortComplex.exact_iff_isZero_right_homology

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

added theorem CategoryTheory.ShortComplex.HomologyData.leftRightHomologyComparison'_eq

added theorem CategoryTheory.ShortComplex.HomologyData.right_homologyIso_eq_left_homologyIso_trans_iso

added theorem CategoryTheory.ShortComplex.hasHomology_of_isIsoLeftRightHomologyComparison

added theorem CategoryTheory.ShortComplex.hasHomology_of_isIso_leftRightHomologyComparison'

added theorem CategoryTheory.ShortComplex.leftRightHomologyComparison'_compatibility

added theorem CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap'

added theorem CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac

added theorem CategoryTheory.ShortComplex.leftRightHomologyComparison'_naturality

added theorem CategoryTheory.ShortComplex.leftRightHomologyComparison_eq

added theorem CategoryTheory.ShortComplex.leftRightHomologyComparison_fac

added theorem CategoryTheory.ShortComplex.π_leftRightHomologyComparison_ι