Commit 2025-06-04 06:26 b3c38642

feat(RepresentationTheory/*): Rep.diagonal k G (n + 1) ≅ Rep.free k G (Fin n → G) (#21736) The first of 2 PRs refactoring group cohomology to use the bar resolution. Given a comm ring k and a group G, the bar resolution 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. This PR defines an isomorphism between the objects in the standard resolution and the bar resolution, i.e. an isomorphism of representations k[Gⁿ⁺¹] ≅ (Gⁿ →₀ k[G]), called Rep.diagonalSuccIsoFree. Moves:

• groupCohomology.resolution.actionDiagonalSucc -> Action.diagonalSuccIsoTensorTrivial
• groupCohomology.resolution.diagonalSucc -> Rep.diagonalSuccIsoTensorTrivial