Commit 2025-06-09 08:15 b2a691d2

feat(RepresentationTheory/*): add the bar resolution (#21738) The third 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 define an isomorphism Rep.diagonalSuccIsoFree between the objects in the standard resolution and bar resolution. In this PR 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.