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}(\bigoplus_{G^n} k[G], A)$, where the righthand side is morphisms in Rep k G, and $k[G]$ is equipped with the left regular representation. If we conjugate the $n$th differential in $\mathrm{Hom}(P, A)$ 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.

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.

To talk about cohomology in low degree, please see the file Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean, which provides API specialized to H⁰, H¹, H².

Main definitions

• 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 complex and the complex $\mathrm{Hom}(P, A),$ where P is the bar resolution of k as a trivial resolution.
• groupCohomology A n: this is $\mathrm{H}^n(G, A),$ defined as the $n$th cohomology of 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

• 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).

@[reducible, inline, deprecated "We now use `(Rep.barComplex k G).linearYonedaObj k A instead" (since := "2025-06-08")]

abbrev groupCohomology.linearYonedaObjResolution {k 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.

Equations

• groupCohomology.linearYonedaObjResolution A = (Rep.standardComplex k G).linearYonedaObj k A

def inhomogeneousCochains.d {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G) (n : ℕ) : ModuleCat.of k ((Fin n → G) → ↑A.V) ⟶ ModuleCat.of k ((Fin (n + 1) → G) → ↑A.V)

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

Equations

• One or more equations did not get rendered due to their size.

theorem inhomogeneousCochains.d_hom_apply {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G) (n : ℕ) (f : (Fin n → G) → ↑A.V) (g : Fin (n + 1) → G) : (ModuleCat.Hom.hom (d A n)) f g = (A.ρ (g 0)) (f fun (i : Fin n) => g i.succ) + ∑ j : Fin (n + 1), (-1) ^ (↑j + 1) • f (j.contractNth (fun (x1 x2 : G) => x1 * x2) g)

theorem inhomogeneousCochains.d_eq {k G : Type u} [CommRing k] [Group G] [DecidableEq G] (A : Rep k G) (n : ℕ) : d A n = CategoryTheory.CategoryStruct.comp (Rep.freeLiftLEquiv (Fin n → G) A).toModuleIso.inv (CategoryTheory.CategoryStruct.comp (((Rep.barComplex k G).linearYonedaObj k A).d n (n + 1)) (Rep.freeLiftLEquiv (Fin (n + 1) → G) A).toModuleIso.hom)

@[reducible, inline]

noncomputable abbrev groupCohomology.inhomogeneousCochains {k G : Type u} [CommRing k] [Group G] [DecidableEq 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.

Equations

• groupCohomology.inhomogeneousCochains A = CochainComplex.of (fun (n : ℕ) => ModuleCat.of k ((Fin n → G) → ↑A.V)) (fun (n : ℕ) => inhomogeneousCochains.d A n) ⋯

theorem groupCohomology.inhomogeneousCochains.ext {k G : Type u} [CommRing k] {n : ℕ} [Group G] [DecidableEq G] {A : Rep k G} {x y : ↑((inhomogeneousCochains A).X n)} (h : ∀ (g : Fin n → G), x g = y g) : x = y

theorem groupCohomology.inhomogeneousCochains.ext_iff {k G : Type u} [CommRing k] {n : ℕ} [Group G] [DecidableEq G] {A : Rep k G} {x y : ↑((inhomogeneousCochains A).X n)} : x = y ↔ ∀ (g : Fin n → G), x g = y g

theorem groupCohomology.inhomogeneousCochains.d_def {k G : Type u} [CommRing k] [Group G] [DecidableEq G] (A : Rep k G) (n : ℕ) : (inhomogeneousCochains A).d n (n + 1) = inhomogeneousCochains.d A n

theorem groupCohomology.inhomogeneousCochains.d_comp_d {k G : Type u} [CommRing k] (n : ℕ) [Group G] [DecidableEq G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (inhomogeneousCochains.d A n) (inhomogeneousCochains.d A (n + 1)) = 0

def groupCohomology.inhomogeneousCochainsIso {k G : Type u} [CommRing k] [Group G] [DecidableEq G] (A : Rep k G) : inhomogeneousCochains A ≅ (Rep.barComplex k G).linearYonedaObj k A

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

Equations

• groupCohomology.inhomogeneousCochainsIso A = HomologicalComplex.Hom.isoOfComponents (fun (i : ℕ) => (Rep.freeLiftLEquiv (Fin i → G) A).toModuleIso.symm) ⋯

@[reducible, inline]

abbrev groupCohomology.cocycles {k G : Type u} [CommRing k] [Group G] [DecidableEq G] (A : Rep k G) (n : ℕ) : ModuleCat k

The n-cocycles Zⁿ(G, A) of a k-linear G-representation A, i.e. the kernel of the nth differential in the complex of inhomogeneous cochains.

Equations

• groupCohomology.cocycles A n = HomologicalComplex.cycles (groupCohomology.inhomogeneousCochains A) n

@[reducible, inline]

abbrev groupCohomology.iCocycles {k G : Type u} [CommRing k] [Group G] [DecidableEq G] (A : Rep k G) (n : ℕ) : cocycles A n ⟶ (inhomogeneousCochains A).X n

The natural inclusion of the n-cocycles Zⁿ(G, A) into the n-cochains Cⁿ(G, A).

Equations

• groupCohomology.iCocycles A n = HomologicalComplex.iCycles (groupCohomology.inhomogeneousCochains A) n

@[reducible, inline]

abbrev groupCohomology.toCocycles {k G : Type u} [CommRing k] [Group G] [DecidableEq G] (A : Rep k G) (i j : ℕ) : (inhomogeneousCochains A).X i ⟶ cocycles A j

This is the map from i-cochains to j-cocycles induced by the differential in the complex of inhomogeneous cochains.

Equations

• groupCohomology.toCocycles A i j = HomologicalComplex.toCycles (groupCohomology.inhomogeneousCochains A) i j

def groupCohomology {k G : Type u} [CommRing k] [Group G] [DecidableEq 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.

Equations

• groupCohomology A n = HomologicalComplex.homology (groupCohomology.inhomogeneousCochains A) n

@[reducible, inline]

abbrev groupCohomology.π {k G : Type u} [CommRing k] [Group G] [DecidableEq G] (A : Rep k G) (n : ℕ) : cocycles A n ⟶ groupCohomology A n

The natural map from n-cocycles to nth group cohomology for a k-linear G-representation A.

Equations

• groupCohomology.π A n = HomologicalComplex.homologyπ (groupCohomology.inhomogeneousCochains A) n

@[deprecated groupCohomology.π (since := "2025-06-11")]

def groupCohomologyπ {k G : Type u} [CommRing k] [Group G] [DecidableEq G] (A : Rep k G) (n : ℕ) : groupCohomology.cocycles A n ⟶ groupCohomology A n

Alias of groupCohomology.π.

---

The natural map from n-cocycles to nth group cohomology for a k-linear G-representation A.

Equations

• @groupCohomologyπ = @groupCohomology.π

theorem groupCohomology_induction_on {k G : Type u} [CommRing k] [Group G] [DecidableEq G] {A : Rep k G} {n : ℕ} {C : ↑(groupCohomology A n) → Prop} (x : ↑(groupCohomology A n)) (h : ∀ (x : ↑(groupCohomology.cocycles A n)), C ((CategoryTheory.ConcreteCategory.hom (groupCohomology.π A n)) x)) : C x

def groupCohomologyIsoExt {k G : Type u} [CommRing k] [Group G] [DecidableEq 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.

Equations

• groupCohomologyIsoExt A n = isoOfQuasiIsoAt (HomotopyEquiv.ofIso (groupCohomology.inhomogeneousCochainsIso A)).hom n ≪≫ (Rep.barResolution.extIso k G A n).symm

theorem isZero_groupCohomology_succ_of_subsingleton {k G : Type u} [CommRing k] [Group G] [Subsingleton G] (A : Rep k G) (n : ℕ) : CategoryTheory.Limits.IsZero (groupCohomology A (n + 1))