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.

5 Responses to Formalising Mathematics : workshop 8 — group cohomology

Mabud Ali Sarkar says:

September 6, 2021 at 4:05 pm

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

LikeLike

- xenaproject says:
  
  September 6, 2021 at 7:17 pm
  
  I don’t understand your question. Is the answer https://github.com/ImperialCollegeLondon/formalising-mathematics ?
  
  LikeLike
  
  - Mabud Ali Sarkar says:
    
    September 6, 2021 at 7:25 pm
    
    You said that the workshop focused on the following topics
    (1)define all the maps in that exact sequence
    (2)prove the sequence is exact
    (3)prove the inflation-restriction sequence is exact
    (4)develop the concrete theory of H^2 via 2-cocycles and 2-coboundaries
    (5)develop the abstract theory of H^n via n-cocycles and n-coboundaries.
    
    My question was, whether these notes available in PDF form or not. I guess the mathlib codes available in the link you attached. Thanks
    
    LikeLike
xenaproject says:

September 6, 2021 at 7:26 pm

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

LikeLike

- Mabud Ali Sarkar says:
  
  September 6, 2021 at 7:29 pm
  
  Ok, thanks. So I have to install the mathlib to work on Lean files.
  
  LikeLike