Commit 2024-01-01 15:59 5683185b

View on Github →

feat(RepresentationTheory/GroupCohomology/LowDegree): Identify groupCohomology A nwith Hn A for n = 0, 1, 2 (#8802)

Estimated changes

Modified Mathlib/RepresentationTheory/GroupCohomology/Basic.lean

Modified Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean

added def groupCohomology.dZeroArrowIso

added theorem groupCohomology.dZero_comp_H0_subtype

added theorem groupCohomology.groupCohomologyπ_comp_isoH0_hom

added theorem groupCohomology.groupCohomologyπ_comp_isoH1_hom

added theorem groupCohomology.groupCohomologyπ_comp_isoH2_hom

added def groupCohomology.isoH0

added def groupCohomology.isoH1

added def groupCohomology.isoH2

added def groupCohomology.isoOneCocycles

added theorem groupCohomology.isoOneCocycles_hom_comp_subtype

added def groupCohomology.isoTwoCocycles

added theorem groupCohomology.isoTwoCocycles_hom_comp_subtype

added def groupCohomology.isoZeroCocycles

added theorem groupCohomology.isoZeroCocycles_hom_comp_subtype

added def groupCohomology.shortComplexH0

added theorem groupCohomology.shortComplexH0_exact

added def groupCohomology.shortComplexH1

added def groupCohomology.shortComplexH1Iso

added def groupCohomology.shortComplexH2

added def groupCohomology.shortComplexH2Iso

added theorem groupCohomology.toCocycles_comp_isoOneCocycles_hom

added theorem groupCohomology.toCocycles_comp_isoTwoCocycles_hom