Commit 2025-05-23 11:14 3ffff9ed
View on Github →refactor(Algebra/Homology/ShortComplex/ModuleCat, RepresentationTheory/GroupCohomology/*): unfold CategoryTheory.ShortComplex.moduleCatLeftHomologyData less eagerly (#24696)
ShortComplex.moduleCatLeftHomologyData represents the homology of a short complex in ModuleCat as a concrete quotient of a LinearMap.ker by a LinearMap.range. When working on the level of linear maps - i.e. ModuleCat.Hom.hom of a morphism in ModuleCat - simp lemmas unfolding this concrete definition are useful. But when reasoning about morphisms in ModuleCat it seems handy not to unfold the definition, so that simp can apply the general LeftHomologyData API.
To that end, this PR replaces simp lemmas ShortComplex.moduleCatLeftHomologyData_i, ShortComplex.moduleCatLeftHomologyData_π with their linear map versions, ShortComplex.moduleCatLeftHomologyData_i_hom, ShortComplex.moduleCatLeftHomologyData_π_hom.
It also rephrases declarations about ModuleCat morphisms in the group cohomology folder in terms of ShortComplex.moduleCatLeftHomologyData rather than unfolding.
Deletions:
- CategoryTheory.ShortComplex.moduleCatHomology
- CategoryTheory.ShortComplex.moduleCatHomologyπ
- CategoryTheory.ShortComplex.moduleCatLeftHomologyData_i
- CategoryTheory.ShortComplex.moduleCatLeftHomologyData_π
- CategoryTheory.ShortComplex.moduleCatLeftHomologyData_f'