Commit 2025-06-16 12:56 6213db69

feat(RepresentationTheory/Homological/GroupHomology/Basic): define group homology (#25868) Let k be a commutative ring and G a group. This PR defines the group homology of A : Rep k G to be the homology of the complex $$\dots \to \bigoplus_{G^2} A \to \bigoplus_{G^1} A \to \bigoplus_{G^0} A$$ (using Finsupp for the objects) with differential $d_n$ sending $a\cdot (g_0, \dots, g_n)$ to $$\rho(g_0^{-1})(a)\cdot (g_1, \dots, g_n) + \sum_{i = 0}^{n - 1}(-1)^{i + 1}a\cdot (g_0, \dots, g_ig_{i + 1}, \dots, g_n) + (-1)^{n + 1}a\cdot (g_0, \dots, g_{n - 1})$$ (where ρ is the representation attached to A). We have a k-linear isomorphism $\bigoplus_{G^n} A \cong (A \otimes_k \left(\bigoplus_{G^n} k[G]\right))_G$ given by Rep.coinvariantsTensorFreeLEquiv. If we conjugate the nth differential in $(A \otimes_k P)_G$ by this isomorphism, where P is the bar resolution of k as a trivial k-linear G-representation, then the resulting map agrees with the differential $d_n$ defined above, a fact we prove. Hence our $d_n$ squares to zero, and we get $\mathrm{H}_n(G, A) \cong \mathrm{Tor}_n(A, k),$ where $\mathrm{Tor}$ is defined by deriving the second argument of the functor $(A, B) \mapsto (A \otimes_k B)_G.$