Commit 2025-06-17 03:55 4f37a8d3

refactor(RepresentationTheory/GroupCohomology): refactor low degree group cohomology (#25870) groupCohomology A n is defined as the abstract homology of the complex of inhomogeneous cochains in RepresentationTheory.GroupCohomology.Basic, whose objects are (Fin n → G) → A, whilst in RepresentationTheory.GroupCohomology.LowDegree we provide alternative definitions of H0, H1, H2 which 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 of G → A and G × G → A respectively and relate these (and Aᴳ) to the original groupCohomology A n for n = 0, 1, 2. This PR implements that.