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

The complex `Hom(P, A)`

, where `P`

is the standard resolution of `k`

as a trivial `k`

-linear
`G`

-representation.

## Instances For

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

## 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`

.

## Instances For

The `n`

th 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.