…oup 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 `n`th 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.$

…25878)

Adds `deprecated_module`s for files moved in #25868.

…oup homology (leanprover-community#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 `n`th 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.$

…eanprover-community#25878)

Adds `deprecated_module`s for files moved in leanprover-community#25868.

…oup homology (leanprover-community#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 `n`th 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.$

…eanprover-community#25878)

Adds `deprecated_module`s for files moved in leanprover-community#25868.