The group cohomology of a k-linear G-representation

Let k be a commutative ring and G a group. This file defines the group cohomology of A : Rep k G to be the cohomology of the complex $$0 \to \mathrm{Fun}(G^0, A) \to \mathrm{Fun}(G^1, A) \to \mathrm{Fun}(G^2, A) \to \dots$$ with differential $d^n$ sending $f: G^n \to A$ to the function mapping $(g_0, \dots, g_n)$ to $$\rho(g_0)(f(g_1, \dots, g_n))

• \sum_{i = 0}^{n - 1} (-1)^{i + 1}\cdot f(g_0, \dots, g_ig_{i + 1}, \dots, g_n)$$ $$+ (-1)^{n + 1}\cdot f(g_0, \dots, g_{n - 1})$$ (where ρ is the representation attached to A).

We have a k-linear isomorphism $\mathrm{Fun}(G^n, A) \cong \mathrm{Hom}(k[G^{n + 1}], A)$, where the righthand side is morphisms in Rep k G, and the representation on $k[G^{n + 1}]$ is induced by the diagonal action of G. If we conjugate the $n$th differential in $\mathrm{Hom}(P, A)$ by this isomorphism, where P is the standard 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.

This gives us for free a proof that our $d^n$ squares to zero. It also gives us an isomorphism $\mathrm{H}^n(G, A) \cong \mathrm{Ext}^n(k, A),$ where $\mathrm{Ext}$ is taken in the category Rep k G.

Main definitions

• GroupCohomology.linearYonedaObjResolution A: a complex whose objects are the representation morphisms $\mathrm{Hom}(k[G^{n + 1}], A)$ and whose cohomology is the group cohomology $\mathrm{H}^n(G, A)$.
• GroupCohomology.inhomogeneousCochains A: a complex whose objects are $\mathrm{Fun}(G^n, A)$ and whose cohomology is the group cohomology $\mathrm{H}^n(G, A).$
• GroupCohomology.inhomogeneousCochainsIso A: an isomorphism between the above two complexes.
• group_cohomology A n: this is $\mathrm{H}^n(G, A),$ defined as the $n$th cohomology of the second complex, inhomogeneousCochains A.
• groupCohomologyIsoExt A n: an isomorphism $\mathrm{H}^n(G, A) \cong \mathrm{Ext}^n(k, A)$ (where $\mathrm{Ext}$ is taken in the category Rep k G) induced by inhomogeneousCochainsIso A.

Implementation notes

Group cohomology is typically stated for G-modules, or equivalently modules over the group ring ℤ[G]. However, ℤ can be generalized to any commutative ring k, which is what we use. Moreover, we express k[G]-module structures on a module k-module A using the Rep definition. We avoid using instances Module (MonoidAlgebra k G) A so that we do not run into possible scalar action diamonds.

TODO

• API for cohomology in low degree: $\mathrm{H}^0, \mathrm{H}^1$ and $\mathrm{H}^2.$ For example, the inflation-restriction exact sequence.
• The long exact sequence in cohomology attached to a short exact sequence of representations.
• Upgrading groupCohomologyIsoExt to an isomorphism of derived functors.
• Profinite cohomology.

Longer term:

• The Hochschild-Serre spectral sequence (this is perhaps a good toy example for the theory of spectral sequences in general).

@[inline, reducible]

abbrev GroupCohomology.linearYonedaObjResolution {k : Type u} {G : Type u} [CommRing k] [Monoid G] (A : Rep k G) : CochainComplex (ModuleCat k) ℕ

The complex Hom(P, A), where P is the standard resolution of k as a trivial k-linear G-representation.

theorem GroupCohomology.linearYonedaObjResolution_d_apply {k : Type u} {G : Type u} [CommRing k] [Monoid G] {A : Rep k G} (i : ℕ) (j : ℕ) (x : HomologicalComplex.X (GroupCohomology.resolution k G) i ⟶ A) : ↑(HomologicalComplex.d (GroupCohomology.linearYonedaObjResolution A) i j) x = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d (GroupCohomology.resolution k G) j i) x

@[simp]

theorem InhomogeneousCochains.d_apply {k : Type u} {G : Type u} [CommRing k] [Monoid G] (n : ℕ) (A : Rep k G) (f : (Fin n → G) → CoeSort.coe A) (g : Fin (n + 1) → G) : ↑(InhomogeneousCochains.d n A) f g = ↑(↑(Rep.ρ A) (g 0)) (f fun i => g (Fin.succ i)) + Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g)

def InhomogeneousCochains.d {k : Type u} {G : Type u} [CommRing k] [Monoid G] (n : ℕ) (A : Rep k G) : ((Fin n → G) → CoeSort.coe A) →ₗ[k] (Fin (n + 1) → G) → CoeSort.coe A

The differential in the complex of inhomogeneous cochains used to calculate group cohomology.

theorem InhomogeneousCochains.d_eq {k : Type u} {G : Type u} [CommRing k] (n : ℕ) [Group G] (A : Rep k G) : InhomogeneousCochains.d n A = CategoryTheory.CategoryStruct.comp (LinearEquiv.toModuleIso (Rep.diagonalHomEquiv n A)).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.d (GroupCohomology.linearYonedaObjResolution A) n (n + 1)) (LinearEquiv.toModuleIso (Rep.diagonalHomEquiv (n + 1) A)).hom)

The theorem that our isomorphism Fun(Gⁿ, A) ≅ Hom(k[Gⁿ⁺¹], A) (where the righthand side is morphisms in Rep k G) commutes with the differentials in the complex of inhomogeneous cochains and the homogeneous linearYonedaObjResolution.

@[inline, reducible]

noncomputable abbrev GroupCohomology.inhomogeneousCochains {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) : CochainComplex (ModuleCat k) ℕ

Given a k-linear G-representation A, this is the complex of inhomogeneous cochains $$0 \to \mathrm{Fun}(G^0, A) \to \mathrm{Fun}(G^1, A) \to \mathrm{Fun}(G^2, A) \to \dots$$ which calculates the group cohomology of A.

def GroupCohomology.inhomogeneousCochainsIso {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) : GroupCohomology.inhomogeneousCochains A ≅ GroupCohomology.linearYonedaObjResolution A

Given a k-linear G-representation A, the complex of inhomogeneous cochains is isomorphic to Hom(P, A), where P is the standard resolution of k as a trivial G-representation.

def groupCohomology {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (n : ℕ) : ModuleCat k

The group cohomology of a k-linear G-representation A, as the cohomology of its complex of inhomogeneous cochains.

def groupCohomologyIsoExt {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (n : ℕ) : groupCohomology A n ≅ ((Ext k (Rep k G) n).obj (Opposite.op (Rep.trivial k G k))).obj A

The nth group cohomology of a k-linear G-representation A is isomorphic to Extⁿ(k, A) (taken in Rep k G), where k is a trivial k-linear G-representation.