Commit 2023-11-02 20:10 ec3e666d

View on Github →

feat: functoriality of the homology of homological complexes (#8113)

Estimated changes

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

added def HomologicalComplex.ExactAt

added theorem HomologicalComplex.cyclesMap_comp

added theorem HomologicalComplex.cyclesMap_i

added theorem HomologicalComplex.cyclesMap_id

added theorem HomologicalComplex.cyclesMap_zero

added theorem HomologicalComplex.exactAt_iff'

added theorem HomologicalComplex.exactAt_iff

added theorem HomologicalComplex.exactAt_iff_isZero_homology

added theorem HomologicalComplex.homologyMap_comp

added theorem HomologicalComplex.homologyMap_id

added theorem HomologicalComplex.homologyMap_zero

added theorem HomologicalComplex.homology_π_ι

added theorem HomologicalComplex.homologyι_naturality

added theorem HomologicalComplex.homologyπ_naturality

added theorem HomologicalComplex.liftCycles_comp_cyclesMap

added theorem HomologicalComplex.opcyclesMap_comp

added theorem HomologicalComplex.opcyclesMap_comp_descOpcycles

added theorem HomologicalComplex.opcyclesMap_id

added theorem HomologicalComplex.opcyclesMap_zero

added theorem HomologicalComplex.p_opcyclesMap