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 (group law
+) and a subgroup , and let be the quotient group. Say we have an action of a group (group law
*) on , and say is -stable, so gets an induced -action too. Now take -invariants of everything and denote this . The -invariants of are still a subgroup of , but , the -invariant elements of , might be bigger than the image of in . For example if is the integers mod 4, with the cyclic group of order 2 acting by sending to , then is -stable but one checks that acts trivially on so the map is no longer surjective.
Here is an attempt to “measure” failure of surjectivity. Say is -invariant. Lift randomly to . Then if we see that maps to in so must be in . Trying this example in the case above you can convince yourself that you get a group isomorphism from to this way. But in general the map sending to is not a group homomorphism, and is not even “canonical”, as a mathematician would say — it depends on a choice of lifting . Different choices differ by an element of , and asking whether the function is of the form for some is the same as asking whether our original element lifts to an element of .
These ideas synthesized into the following definitions. Say acts on . The zero-th cohomology group is just the subgrup of -invariant elements.
A cocycle for a -action on is a function such that . A coboundary is a cocycle of the form for some . The quotient of the cocycles by the coboundaries is called the first cohomology group .
The construction above shows that if is a -module with a subgroup also preserved by and quotient (people write “a short exact sequence of -modules”) then there is a map . This actually forms part of a seven term long exact sequence:
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.
`Sir, This note is very interesting. However this is the introduction part. How to get full workshop note ?
I don’t understand your question. Is the answer https://github.com/ImperialCollegeLondon/formalising-mathematics ?
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
Yeah, sorry, there are no pdf notes for anything. The course was a series of workshops based on Lean files and blog posts.
Ok, thanks. So I have to install the mathlib to work on Lean files.