Commit 2025-02-19 09:43 289b95fb

View on Github →

refactor(RepresentationTheory/GroupCohomology/LowDegree): make nCoboundaries a submodule of the n-cochains rather than the nCocycles for n = 0, 1, 2 (#22047)

Estimated changes

Modified Mathlib/RepresentationTheory/GroupCohomology/Hilbert90.lean

Modified Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean

modified theorem groupCohomology.H1π_eq_zero_iff

modified theorem groupCohomology.H2π_eq_zero_iff

added theorem groupCohomology.dOne_apply_mem_twoCocycles

added theorem groupCohomology.dZero_apply_mem_oneCocycles

added theorem groupCohomology.isMulOneCoboundary_of_mem_oneCoboundaries

deleted theorem groupCohomology.isMulOneCoboundary_of_oneCoboundaries

added theorem groupCohomology.isMulOneCocycle_of_mem_oneCocycles

deleted theorem groupCohomology.isMulOneCocycle_of_oneCocycles

added theorem groupCohomology.isMulTwoCoboundary_of_mem_twoCoboundaries

deleted theorem groupCohomology.isMulTwoCoboundary_of_twoCoboundaries

added theorem groupCohomology.isMulTwoCocycle_of_mem_twoCocycles

deleted theorem groupCohomology.isMulTwoCocycle_of_twoCocycles

added theorem groupCohomology.isOneCoboundary_of_mem_oneCoboundaries

deleted theorem groupCohomology.isOneCoboundary_of_oneCoboundaries

added theorem groupCohomology.isOneCocycle_of_mem_oneCocycles

deleted theorem groupCohomology.isOneCocycle_of_oneCocycles

added theorem groupCohomology.isTwoCoboundary_of_mem_twoCoboundaries

deleted theorem groupCohomology.isTwoCoboundary_of_twoCoboundaries

added theorem groupCohomology.isTwoCocycle_of_mem_twoCocycles

deleted theorem groupCohomology.isTwoCocycle_of_twoCocycles

deleted theorem groupCohomology.mem_oneCoboundaries_iff

deleted theorem groupCohomology.mem_range_of_mem_oneCoboundaries

deleted theorem groupCohomology.mem_range_of_mem_twoCoboundaries

deleted theorem groupCohomology.mem_twoCoboundaries_iff

added theorem groupCohomology.oneCoboundaries.coe_mk

added theorem groupCohomology.oneCoboundaries.val_eq_coe

modified def groupCohomology.oneCoboundaries

deleted def groupCohomology.oneCoboundariesOfEq

deleted theorem groupCohomology.oneCoboundariesOfEq_apply

deleted def groupCohomology.oneCoboundariesOfMemRange

added theorem groupCohomology.oneCoboundariesToOneCocycles_apply

added theorem groupCohomology.oneCoboundaries_ext

added theorem groupCohomology.oneCoboundaries_le_oneCocycles

deleted theorem groupCohomology.oneCoboundaries_of_mem_range_apply

added theorem groupCohomology.twoCoboundaries.coe_mk

added theorem groupCohomology.twoCoboundaries.val_eq_coe

modified def groupCohomology.twoCoboundaries

deleted def groupCohomology.twoCoboundariesOfEq

deleted theorem groupCohomology.twoCoboundariesOfEq_apply

deleted def groupCohomology.twoCoboundariesOfMemRange

deleted theorem groupCohomology.twoCoboundariesOfMemRange_apply

added theorem groupCohomology.twoCoboundariesToTwoCocycles_apply

added theorem groupCohomology.twoCoboundaries_ext

added theorem groupCohomology.twoCoboundaries_le_twoCocycles