Commit 2025-02-18 17:20 f88c7691

View on Github →

refactor(RepresentationTheory/GroupCohomology/LowDegree): define Hn using ShortComplex.moduleCatHomology for n = 0, 1, 2 (#22046)

Estimated changes

Modified Mathlib/RepresentationTheory/GroupCohomology/Hilbert90.lean

Modified Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean

deleted theorem groupCohomology.H1LequivOfIsTrivial_comp_H1_π

added theorem groupCohomology.H1LequivOfIsTrivial_comp_H1π

deleted def groupCohomology.H1_π

added theorem groupCohomology.H1π_eq_zero_iff

deleted def groupCohomology.H2_π

added theorem groupCohomology.H2π_eq_zero_iff

deleted theorem groupCohomology.dZero_comp_H0_subtype

added theorem groupCohomology.dZero_comp_subtype

modified def groupCohomology.isoH0

modified def groupCohomology.isoH1

modified def groupCohomology.isoH2

modified def groupCohomology.isoZeroCocycles