Commit 2025-06-13 18:23 8e87a390

View on Github →

feat(RepresentationTheory/GroupCohomology): extra lemmas (#25815) Extra lemmas about group cohomology in preparation for #25310.

Estimated changes

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

deleted def CategoryTheory.ShortComplex.moduleCatToCycles

Modified Mathlib/RepresentationTheory/GroupCohomology/Basic.lean

added theorem groupCohomology.inhomogeneousCochains.ext

added theorem groupCohomology_induction_on

Modified Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean

deleted theorem groupCohomology.cochainsMap_id_f_eq_compLeft

added theorem groupCohomology.cochainsMap_id_f_hom_eq_compLeft

added theorem groupCohomology.cocyclesMap_comp

added theorem groupCohomology.cocyclesMap_id

added theorem groupCohomology.map_comp

added theorem groupCohomology.map_id

added theorem groupCohomology.π_map

Modified Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean

added theorem groupCohomology.eq_dOne_comp_inv

added theorem groupCohomology.eq_dTwo_comp_inv

added theorem groupCohomology.eq_dZero_comp_inv

deleted theorem groupCohomology.groupCohomologyπ_comp_isoH0_hom

deleted theorem groupCohomology.groupCohomologyπ_comp_isoH1_hom

deleted theorem groupCohomology.groupCohomologyπ_comp_isoH2_hom

added theorem groupCohomology.isoOneCocycles_inv_comp_iCocycles

added theorem groupCohomology.isoTwoCocycles_inv_comp_iCocycles

added theorem groupCohomology.oneCocycles.dOne_apply

modified def groupCohomology.shortComplexH1Iso

added theorem groupCohomology.twoCocycles.dTwo_apply

added theorem groupCohomology.π_comp_isoH0_hom

added theorem groupCohomology.π_comp_isoH1_hom

added theorem groupCohomology.π_comp_isoH2_hom