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.
To talk about cohomology in low degree, please see the file
Mathlib.RepresentationTheory.GroupCohomology.LowDegree, which gives simpler expressions for
H⁰, H¹, H² than the definition groupCohomology in this file.
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.groupCohomology 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 categoryRep k G) induced byinhomogeneousCochainsIso 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
groupCohomologyIsoExtto 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).
The complex Hom(P, A), where P is the standard resolution of k as a trivial k-linear
G-representation.
Equations
- groupCohomology.linearYonedaObjResolution A = (groupCohomology.resolution k G).linearYonedaObj k A
Instances For
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.
Instances For
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.
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) → CoeSort.coe A)) (fun (n : ℕ) => inhomogeneousCochains.d n A) ⋯
Instances For
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.
Equations
- groupCohomology.inhomogeneousCochainsIso A = HomologicalComplex.Hom.isoOfComponents (fun (i : ℕ) => (Rep.diagonalHomEquiv i A).toModuleIso.symm) ⋯
Instances For
The natural inclusion of the n-cocycles Zⁿ(G, A) into the n-cochains Cⁿ(G, A).
Equations
Instances For
This is the map from i-cochains to j-cocycles induced by the differential in the complex of
inhomogeneous cochains.
Equations
Instances For
The natural map from n-cocycles to nth group cohomology for a k-linear
G-representation A.
Equations
Instances For
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 ≪≫ (groupCohomology.extIso k G A n).symm