Commit 2025-06-02 12:11 04cfb62b

feat(RepresentationTheory/Coinvariants): more API about the coinvariants of a representation (#21735) In this PR we add more API for the coinvariants of a representation (V, ρ):

• Representation.coinvariantsFinsuppLEquiv ρ α: given a type α, this is the k-linear equivalence between (α →₀ V)_G and α →₀ V_G.
• Representation.coinvariantsTprodLeftRegularLEquiv ρ: the k-linear equivalence between (V ⊗[k] k[G])_G and V sending ⟦v ⊗ single g r⟧ ↦ r • ρ(g⁻¹)(v).
• Rep.coinvariantsTensor k G: the functor sending representations A, B to (A ⊗[k] B)_G. This is naturally isomorphic to the functor sending A, B to A ⊗[k[G]] B, where we give A the k[G]ᵐᵒᵖ-module structure defined by g • a := A.ρ g⁻¹ a.
• Rep.coinvariantsTensorFreeLEquiv A α: given a representation A and a type α, this is the k-linear equivalence between (A ⊗ (α →₀ k[G]))_G and α →₀ A sending ⟦a ⊗ single x (single g r)⟧ ↦ single x (r • ρ(g⁻¹)(a)). This is useful for group homology.