refactor(RepresentationTheory/GroupCohomology): refactor low degree group cohomology#25310
refactor(RepresentationTheory/GroupCohomology): refactor low degree group cohomology#25310101damnations wants to merge 45 commits intomasterfrom
Conversation
PR summary 8e87a39073Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
…ver-community/mathlib4 into arlcohlowdegrefactor2
…-community/mathlib4 into arlcohlowdegrefactor
…ver-community/mathlib4 into arlcohlowdegrefactor2
…-community/mathlib4 into arlcohlowdegrefactor
…lib4 into arlcohlowdegrefactor
…-community/mathlib4 into arlcohlowdegrefactor
Extra lemmas about group cohomology in preparation for #25310.
|
This PR/issue depends on: |
…lib4 into arlcohlowdegrefactor
|
This PR has been migrated to a fork-based workflow: #25870 |
…community#25815) Extra lemmas about group cohomology in preparation for leanprover-community#25310.
…community#25815) Extra lemmas about group cohomology in preparation for leanprover-community#25310.
…community#25815) Extra lemmas about group cohomology in preparation for leanprover-community#25310.
…community#25815) Extra lemmas about group cohomology in preparation for leanprover-community#25310.
groupCohomology A nis defined as the abstract homology of the complex of inhomogeneous cochains inRepresentationTheory.GroupCohomology.Basic, whose objects are(Fin n → G) → A, whilst inRepresentationTheory.GroupCohomology.LowDegreewe provide alternative definitions ofH0, H1, H2which are more concrete. But these extra definitions are not worth the extra API they necessitate, as long as we define the (one/two)-co(cycles/boundaries) as submodules ofG → AandG × G → Arespectively and relate these (and Aᴳ) to the originalgroupCohomology A nforn = 0, 1, 2. This PR implements that.