feat(RepresentationTheory/Homological/GroupHomology/Basic): define group homology#21740
feat(RepresentationTheory/Homological/GroupHomology/Basic): define group homology#21740101damnations wants to merge 235 commits intomasterfrom
Conversation
| Note that the existing definition of `Tor` in `Mathlib.CategoryTheory.Monoidal.Tor` is for monoidal | ||
| categories, and the bifunctor we use here does not define a monoidal structure on `Rep k G` in | ||
| general. It corresponds to tensoring modules over `k[G]`, but currently mathlib's `TensorProduct` | ||
| is only defined for commutative rings. |
There was a problem hiding this comment.
I'm a bit confused by this. If G is nonabelian then the tensor product of two (left) k[G]-modules probably can't be done over k[G], and the tensor product of a left module and a right module will only be an abelian group. Isn't what's going on something more subtle, and not purely ring-theoretic, where G acts on a tensor product in some diagonal way, and in particular the definition depends on "which elements of the ring are actually in the group"? Or have I misunderstood? I just don't get what "It corresponds to tensoring modules over k[G]" can mean.
There was a problem hiding this comment.
Thanks, I've made the comment clearer and added "It 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", so yeah it's a k-module but not a k[G]-module in general.
Mathlib/RepresentationTheory/Homological/GroupHomology/Basic.lean
Outdated
Show resolved
Hide resolved
kbuzzard
left a comment
There was a problem hiding this comment.
This looks great to me -- thanks and congratulations! TIL the edge behaviour of contractNth (it can also send (g0,g1,...,gn) to (g0,g1,...,g(n-1)) without doing any multiplication -- for a while I was very confused!)
|
This PR has been migrated to a fork-based workflow: #25868 |
Let
$$\dots \to \bigoplus_{G^2} A \to \bigoplus_{G^1} A \to \bigoplus_{G^0} A$$ $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 $\bigoplus_{G^n} A \cong (A \otimes_k \left(\bigoplus_{G^n} k[G]\right))_G$ given by $(A \otimes_k P)_G$ by this isomorphism, where $d_n$ defined above, a fact we prove.$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.$
kbe a commutative ring andGa group. This PR defines the group homology ofA : Rep k Gto be the homology of the complex(using
Finsuppfor the objects) with differentialρis the representation attached toA).We have a
k-linear isomorphismRep.coinvariantsTensorFreeLEquiv. If we conjugate thenth differential inPis the bar resolution ofkas a trivialk-linearG-representation, then the resulting map agrees with the differentialHence our
Action.rhoaMonoidHominstead of a morphism inMonCat#21652Finsupp#21732Rep.diagonal k G (n + 1) ≅ Rep.free k G (Fin n → G)#21736