Documentation

Mathlib.RepresentationTheory.GroupCohomology.Basic

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 RepresentationTheory.GroupCohomology.LowDegree, which gives simpler expressions for H⁰, H¹, H² than the definition groupCohomology in this file.

Main definitions #

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 #

Longer term:

@[reducible, inline]

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

Equations
Instances For
    @[simp]
    theorem inhomogeneousCochains.d_apply {k : Type u} {G : Type u} [CommRing k] [Monoid G] (n : ) (A : Rep k G) (f : (Fin nG)CoeSort.coe A) (g : Fin (n + 1)G) :
    (inhomogeneousCochains.d n A) f g = (A (g 0)) (f fun (i : Fin n) => g i.succ) + j : Fin (n + 1), (-1) ^ (j + 1) f (j.contractNth (fun (x x_1 : G) => x * x_1) g)
    def inhomogeneousCochains.d {k : Type u} {G : Type u} [CommRing k] [Monoid G] (n : ) (A : Rep k G) :
    ((Fin nG)CoeSort.coe A) →ₗ[k] (Fin (n + 1)G)CoeSort.coe A

    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.

      @[reducible, inline]
      noncomputable abbrev groupCohomology.inhomogeneousCochains {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) :

      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
      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
        Instances For
          @[reducible, inline]
          abbrev groupCohomology.cocycles {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (n : ) :

          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
          Instances For
            @[reducible, inline]
            abbrev groupCohomology.iCocycles {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (n : ) :

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

            Equations
            Instances For
              @[reducible, inline]
              abbrev groupCohomology.toCocycles {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (i : ) (j : ) :

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

              Equations
              Instances For
                def groupCohomology {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (n : ) :

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

                Equations
                Instances For
                  @[reducible, inline]
                  abbrev groupCohomologyπ {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (n : ) :

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

                  Equations
                  Instances For
                    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.

                    Equations
                    Instances For