Commit 2023-09-19 11:09 dd7a1c24

View on Github →

feat: relations between cycles, opcycles and homology of short complexes (#7194)

Estimated changes

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

added theorem CategoryTheory.ShortComplex.LeftHomologyData.homologyIso_hom_comp_leftHomologyIso_inv

added theorem CategoryTheory.ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom

added theorem CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso_hom_comp_homologyIso_inv

added theorem CategoryTheory.ShortComplex.LeftHomologyData.π_comp_homologyIso_inv

added theorem CategoryTheory.ShortComplex.RightHomologyData.homologyIso_hom_comp_rightHomologyIso_inv

added theorem CategoryTheory.ShortComplex.RightHomologyData.homologyIso_hom_comp_ι

added theorem CategoryTheory.ShortComplex.RightHomologyData.homologyIso_inv_comp_homologyι

added theorem CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_comp_homologyIso_inv

added theorem CategoryTheory.ShortComplex.comp_homologyMap_comp

added theorem CategoryTheory.ShortComplex.homology_π_ι

added theorem CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles

added theorem CategoryTheory.ShortComplex.homologyι_naturality

added theorem CategoryTheory.ShortComplex.homologyπ_comp_leftHomologyIso_inv:

added theorem CategoryTheory.ShortComplex.homologyπ_naturality

added theorem CategoryTheory.ShortComplex.liftHomology_ι

added theorem CategoryTheory.ShortComplex.rightHomologyIso_hom_comp_homologyι

added theorem CategoryTheory.ShortComplex.toCycles_comp_homologyπ

added theorem CategoryTheory.ShortComplex.π_descHomology

added theorem CategoryTheory.ShortComplex.π_homologyMap_ι