Mathlib Changelog
v4
Changelog
About
Github
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