Commit 2025-06-07 09:38 e9d22cd4

feat(RepresentationTheory/*): prerequisites for the bar resolution (#25546) The second of 3 PRs refactoring group cohomology to use the bar resolution. Given a comm ring k and a group G, this is the projective resolution of k as a trivial G-representation whose nth object is Gⁿ →₀ k[G] with representation defined pointwise by the left regular representation on k[G], and whose differentials send (g₀, ..., gₙ) to g₀·(g₁, ..., gₙ) + ∑ (-1)ʲ⁺¹·(g₀, ..., gⱼgⱼ₊₁, ..., gₙ) + (-1)ⁿ⁺¹·(g₀, ..., gₙ₋₁) for j = 0, ... , n - 1. The refactor means we can reuse this material to set up group homology. In #21736 we defined an isomorphism Rep.diagonalSuccIsoFree between the objects in the standard resolution and bar resolution. In the next PR, #21738, we show that this isomorphism defines a commutative square with the respective differentials, and thus conclude that the bar resolution differential squares to zero and that the 2 complexes are isomorphic. We carry the exactness properties across this isomorphism to conclude the bar resolution is a projective resolution too, in Rep.barResolution. In this PR we factor out some material from #21738, to make it easier to review.