non-abelian group cohomology

Stream: mathlib4

[Wang Jingting]

@Kevin Buzzard Could you suggest a reference if a fully general version of non-Abelian group cohomology is possible to be defined? I think we tried to do some searching before formalizing this but didn't find anything more general.

[Notification Bot]

A message was moved here from #general > Question about to_additive by Kevin Buzzard.

[Kevin Buzzard]

@Wang Jingting I have moved your question to a more appropriate thread (the previous one is about the issues with to_additive; the below is an independent mathematical question).

Wang Jingting said:

Kevin Buzzard Could you suggest a reference if a fully general version of non-Abelian group cohomology is possible to be defined? I think we tried to do some searching before formalizing this but didn't find anything more general.

Although I don't know the area myself, my understanding is that there are exotic ways of doing nonabelian cohomology involving gerbes and other fancy things like that.

Here is my understanding of group cohomology (of abelian groups). Historically humans discovered $H^n$ for $n\leq 2$ first, often as n-cocycles over n-coboundaries. These ideas (plus clunky calculation proofs relating different cohomology groups) were enough to push through the first proofs of global class field theory. Later on it was discovered that these constructions were a special case of a general theory $H^n(G,A)$ of group cohomology, which could be used to streamline and simplify the original proofs. However it's still important to have an "explicit" version of the theory in low degree $n\leq 2$, because sometimes (for example when doing a diagram chase or a construction of an element of a cohomology group from some other mathematical object) it's really important to have access to the 1-cocycle or 2-cocycle; furthermore sometimes a 2-cocycle might contain more information than the corresponding cohomology class, which one occasionally wants to keep track of (analogous to how we sometimes pick a basis for a vector space).

As a result, mathlib's set-up for group cohomology involves a general $H^n$ definition, and then special API for degrees $n\leq 2$ where one can define $1$- and $2$-cocycles explicitly (rather than having them be $n$-cocycles for $n=1$ or $n=2$; an analogue would be being able to refer to an element of ℝ or ℝ × ℝ rather than having to talk about an element of Fin n → R for n=1 or 2). We have been stress-testing this definition in the class field theory repo and it seems to be holding up well.

Historically the development of abelian group cohomology in mathlib went like this: first I gave a 3rd year undergraduate the project of developing H^1 and H^2, and then I gave a Masters student the project of developing H^n for all n, and then I gave a PhD student the project of developing H^n whilst avoiding all the mistakes that I'd made when working with the other students, and got the PhD student to PR things to mathlib.

With nonabelian cohomology I feel like there are several questions which we might want to consider before starting on PRing material. Firstly, should there be some kind of crazy nonabelian cohomology approach which we set things up using fancy stuff and then restrict to degree at most 2? Secondly, what should the relationship be between the abelian and the nonabelian theory? I don't immediately have the answer to either of these questions but at least I feel like they should be discussed.

[Kevin Buzzard]

It might well be the case that there is a good argument for setting up the low-degree theory in an elementary way in the non-abelian setting. I am going on about gerbes and stacks and what have you but I don't know anything about the details here, all I know is that French people write complicated books about the theory. However in the abelian case I became convinced during the time I was supervising the students that developing a low-degree theory was not the best way to approach things for mathlib, and what we should do instead is what we have done in mathlib, i.e., developing a fancy theory which works in general and then making all the API to show that in low degree it could be treated exactly like the low-level definition.

In your situation this simply might not apply, and perhaps the approach is to avoid all this fancy stuff and just do what you're doing.

The other thing worth discussing is how to relate this to the abelian case. In the abelian case we have explicit definitions for n-cocycles and n-coboundaries for n<=2; should these be generalised to the nonabelian case? Can they be generalised? If they can, should you be using these instead? I am a bit worried about relating nonabelian cohomology to abelian cohomology when the not-necessarily-abelian group is actually abelian. Hmm, looking at the definition of docs#groupCohomology.cocycles₁ maybe it will be hopeless trying to reuse this theory. At the very least I think that you might want to stick to the notation that we're using in the abelian case.

These are just vague thoughts but I thought I should raise them.

[Wang Jingting]

Yeah, I agree with you on that the current way of formalizing (Abelian) group cohomology in mathlib is the right way to do - first develop the general theory and then specialize to n = 1, 2.

For the part about relating nonabelian cohomology to abelian case, we have already constructed isomorphisms between the (explicitly constructed) non abelian group cohomology and abelian version for n = 0, 1 and proved that these isomorphisms commutes with H0.map and the connection homomorphism.

(We also have Z1 corresponding to docs#groupCohomology.cocycles₁, and the equivalence between them)

If you think it's necessary, we could certainly change the notations to match the abelian version.

[Scott Carnahan]

I think people may have a use for formalized nonabelian H^1 in the near future - there are applications in many areas of math. On the other hand, it may be a very long time before anyone needs a formalization of higher nonabelian cohomology. So, I would suggest focusing on H^1 for now.
By the way, the basic reference is Giraud’s “Cohomologie Non-abelienne” (spelling may be wrong)

[Kevin Buzzard]

As I just said on the PR, I think that setting things up for AddGroup is a terrible idea. All the examples of non-abelian cohomology I know have group law multiplication, I don't know of a single example in mathematics of a group with group law written as addition which is not commutative, and finally mathlib's philosophy is "multiplicative case first, and if you want the additive case then to_additive it". So right now I would say that this PR should be multiplicativised.