Formalising Mathematics : workshop 8 — group cohomology

This is notes on the last of the eight workshops I am running this term as part of an EPSRC Taught Course Centre course. Many thanks to the students for coming, it was very interesting working with you all.

I promised I would do something more ambitious in week 8, and eventually I settled on group cohomology. I usually write these blog posts just before the workshop but instead this week I wrote a README and am only now writing this more detailed document after the event.

What is group cohomology?

I don’t know the history of group cohomology, but I do know that it’s possible to invent the theory of 1-cocycles in lots of ways (for example when trying to understand what the top right hand corner of a group homomorphism from a group G into 2×2 upper triangular matrices “is”) and so they were bound to show up eventually. The basic question is this: Say we have an abelian group N (group law +) and a subgroup M, and let P:=N/M be the quotient group. Say we have an action of a group (group law *) G on N, and say M is G-stable, so P gets an induced G-action too. Now take G-invariants of everything and denote this N\mapsto N^G. The G-invariants M^G of M are still a subgroup of N^G, but P^G, the G-invariant elements of P, might be bigger than the image of N^G in P. For example if N=\mathbb{Z}/4\mathbb{Z} is the integers mod 4, with G the cyclic group of order 2 acting by sending x to -x, then M:=N^G=\{0,2\} is G-stable but one checks that G acts trivially on P so the map N^G\to P^G is no longer surjective.

Here is an attempt to “measure” failure of surjectivity. Say p\in P is G-invariant. Lift randomly to n\in N. Then if g\in G we see that gn-n maps to gp-p=0 in P so must be in M. Trying this example in the \mathbb{Z}/4\mathbb{Z} case above you can convince yourself that you get a group isomorphism from G to M this way. But in general the map G\to M sending g to gn-n is not a group homomorphism, and is not even “canonical”, as a mathematician would say — it depends on a choice of n lifting p. Different choices differ by an element of m, and asking whether the function g\mapsto gn-n is of the form g\mapsto gm-m for some m\in M is the same as asking whether our original element p\in P^G lifts to an element of N^G.

These ideas synthesized into the following definitions. Say G acts on M. The zero-th cohomology group H^0(G,M) is just the subgrup M^G of G-invariant elements.

A cocycle for a G-action on M is a function c:G\to M such that c(gh)=c(g)+gc(h). A coboundary is a cocycle of the form g\mapsto gm-m for some m\in M. The quotient of the cocycles by the coboundaries is called the first cohomology group H^1(G,M).

The construction above shows that if N is a G-module with a subgroup M also preserved by G and quotient P=N/M (people write “a short exact sequence of G-modules”) then there is a map H^0(G,P)\to H^1(G,M). This actually forms part of a seven term long exact sequence:

0 \to H^0(G,M)\to H^0(G,N)\to H^0(G,P)\to H^1(G,M)\to H^1(G,N)\to H^1(G,P)

and our goal in this workshop, at least if we had infinite time, would be to:

  • define all the maps in that exact sequence
  • prove the sequence is exact
  • prove the inflation-restriction sequence is exact
  • develop the concrete theory of H^2 via 2-cocycles and 2-coboundaries
  • develop the abstract theory of H^n via n-cocycles and n-coboundaries.

My 2018 BSc project student Anca Ciobanu achived the first two of these goals and my 2019 MSc project student Shenyang Wu achieved the last one. So these goals are definitely possible! It will take rather longer than 2 hours though.

This has become a mini-project of mine, and my current thoughts can be seen in the ideas directory of the week 8 folder in the GitHub workshop repository. Ultimately I hope to get this stuff into mathlib (or perhaps to persuade someone else to get it into mathlib for me 😉 )

If you weren’t part of the workshop then you can still do it yourself, all you need is a working Lean and mathlib installation, which you can get following the instructions on the Leanprover community website.


About xenaproject

The Xena Project aims to get mathematics undergraduates (at Imperial College and beyond) trained in the art of formalising mathematics on a computer. Why? Because I have this feeling that digitising mathematics will be really important one day.
This entry was posted in Uncategorized. Bookmark the permalink.

5 Responses to Formalising Mathematics : workshop 8 — group cohomology

  1. Mabud Ali Sarkar says:

    `Sir, This note is very interesting. However this is the introduction part. How to get full workshop note ?


  2. xenaproject says:

    Yeah, sorry, there are no pdf notes for anything. The course was a series of workshops based on Lean files and blog posts.


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s