Commit 2023-10-27 09:57 02b5c76b

View on Github →

feat(RepresentationTheory/GroupCohomology): add some API for group cohomology in low degree (#7734)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RepresentationTheory/GroupCohomology/Basic.lean

added theorem groupCohomology.inhomogeneousCochains.d_def

Created Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean

added def groupCohomology.H1_π

added def groupCohomology.H2_π

added def groupCohomology.dOne

added theorem groupCohomology.dOne_comp_dZero

added theorem groupCohomology.dOne_comp_eq

added def groupCohomology.dTwo

added theorem groupCohomology.dTwo_comp_dOne

added theorem groupCohomology.dTwo_comp_eq

added def groupCohomology.dZero

added theorem groupCohomology.dZero_comp_eq

added theorem groupCohomology.dZero_ker_eq_invariants

added theorem groupCohomology.mem_oneCoboundaries_of_dZero_apply

added theorem groupCohomology.mem_oneCoboundaries_of_mem_range

added theorem groupCohomology.mem_oneCocycles_def

added theorem groupCohomology.mem_oneCocycles_iff

added theorem groupCohomology.mem_range_of_mem_oneCoboundaries

added theorem groupCohomology.mem_range_of_mem_twoCoboundaries

added theorem groupCohomology.mem_twoCoboundaries_of_dOne_apply

added theorem groupCohomology.mem_twoCoboundaries_of_mem_range

added theorem groupCohomology.mem_twoCocycles_def

added theorem groupCohomology.mem_twoCocycles_iff

added def groupCohomology.oneCoboundaries

added def groupCohomology.oneCochainsLinearEquiv

added def groupCohomology.oneCocycles

added theorem groupCohomology.oneCocycles_map_inv

added theorem groupCohomology.oneCocycles_map_one

added def groupCohomology.threeCochainsLinearEquiv

added def groupCohomology.twoCoboundaries

added def groupCohomology.twoCochainsLinearEquiv

added def groupCohomology.twoCocycles

added theorem groupCohomology.twoCocycles_map_one_fst

added theorem groupCohomology.twoCocycles_map_one_snd

added theorem groupCohomology.twoCocycles_ρ_map_inv_sub_map_inv

added def groupCohomology.zeroCochainsLinearEquiv