Commit 2025-05-19 05:18 e88c9842

View on Github →

feat: TopModuleCat is a CategoryWithHomology (#24976) Coauthored-by: Richard Hill

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/ModuleCat/Topology/Homology.lean

added def TopModuleCat.cokerπ

added theorem TopModuleCat.cokerπ_surjective

added theorem TopModuleCat.comp_cokerπ

added theorem TopModuleCat.hom_cokerπ

added def TopModuleCat.isColimitCoker

added def TopModuleCat.isLimitKer

added def TopModuleCat.kerι

added theorem TopModuleCat.kerι_apply

added theorem TopModuleCat.kerι_comp

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

added theorem CategoryTheory.ShortComplex.map_leftRightHomologyComparison'

Modified Mathlib/Topology/Category/TopCat/Basic.lean

added theorem TopCat.isIso_iff_isHomeomorph