group cohomology

Stream: maths

[Kevin Buzzard]

So I'm embarking on group cohomology with an MSc student @Shenyang Wu and we're defining d on cochains. As part of the definition we have these "contraction" maps F (n : nat) (j : fin (n + 1)) (g : fin (n + 1) -> G) : fin n -> G with definition lam k, if k < j then g k else if k = j then (g j) * (g (j + 1)) else g (k + 1) and we'll need a lemma of the form F n k \circ F (n + 1) j = something like F n j \circ F (n + 1) k except that depending on whether j<k or k<j some j should be a j-1 or maybe some k should be a k-1. This is all no doubt some fundamental construction in some category of simplicial sets or something. @Reid Barton @Scott Morrison is what we need already in mathlib or available somewhere else, so we're not re-inventing the wheel? We need to understand F to prove d^2=0.

[Reid Barton]

@Johan Commelin proved that the chain complex of a simplicial abelian group is a complex (d^2 = 0)

[Kevin Buzzard]

There is another way to set this up, where F (n : nat) (j : fin (n + 1)) (g : fin (n + 1) -> G) : fin n -> G just drops the j'th term

[Reid Barton]

However depending on how you set things up, you might have some difficulty showing that you have a simplicial object

[Reid Barton]

Yes, that way will be a lot easier, I think.

[Kevin Buzzard]

Thanks.

[Reid Barton]

At least, if you want to connect to Johan's work. Because you already have a simplicial object more or less by definition (a simplicial operator just acts by precomposition).

[Reid Barton]

I think Johan's work might have been in a PR that was never merged, let me see if I can find it

[Reid Barton]

Well I found #144, but I think there may have been a second attempt

[Reid Barton]

Hmm, maybe there is only https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/src/category_theory/simplex.lean

[Kevin Buzzard]

Do you have any intention of PR'ing all that stuff?

[Kevin Buzzard]

I want to make group cohomology in Lean and I'm pretty sure that some of those tools are going to be useful for setting up the basics.

[Reid Barton]

I have too big a backlog of things to PR...

[Reid Barton]

But this file doesn't depend on anything else in lean-homotopy-theory at least

[Reid Barton]

In your second setup, are you planning to mod out fin (n + 1) -> G by the diagonal action of G?

[Kevin Buzzard]

I'm wondering whether I can get away with not doing it.

[Reid Barton]

The alternative is to require that 0 is mapped to the identity of G but then the first face map will have a funny formula

[Kevin Buzzard]

https://mathoverflow.net/questions/6950/why-is-the-standard-definition-of-cocycle-the-one-that-always-comes-up

[Kevin Buzzard]

I started by telling @Shenyang Wu to use (fin n -> G) -> M and using the "twisted" d, which involves those maps F I mentioned earlier

[Kevin Buzzard]

and then I realised that working with fin (n + 1) -> G might be easier because the d^2=0 proof looked much easier

[Kevin Buzzard]

but then you have to work around this quotient issue

[Reid Barton]

As one of the answers observed, rather than actually form a quotient, you could then take only G-equivariant functions out of it

[Reid Barton]

G-equivariant functions from fin (n + 1) -> G to M

[Reid Barton]

Actually I guess you have to do it that way maybe?

[Reid Barton]

when M has nontrivial action

[Reid Barton]

Oh, it's even in your question.

[Kevin Buzzard]

I should probably read that question at some point

[Reid Barton]

I'm a little surprised I didn't answer this question

[Kevin Buzzard]

do you know the answer? I remember being not too convinced by any of the topologists' suggestions.

[Reid Barton]

Let me try to give what I think is a better answer

[Kevin Buzzard]

I see cocycles coming up in all sorts of calculations in group theory

[Reid Barton]

I'm not sure exactly how well this will go, but anyways

[Reid Barton]

You should start with the category EG, which has one object for each element of G, and a unique morphism between any pair of objects

[Reid Barton]

This is a "resolution" of the category with one object and one morphism (we know maps out of this are G-fixed points, so this has something to do with group cohomology) as something on which G acts freely, by left multiplication, say

[Reid Barton]

Let's look at the orbits of EG under the action of G

[Reid Barton]

There's obviously just one orbit of objects. For morphisms, if we have a morphism from x to y, give it the label x^{-1} y. Then g sends it to a morphism from gx to gy with the same label (gx)^{-1} gy = x^{-1} y. It's easy to see morphisms with the same label make up the orbits.

[Reid Barton]

Moreover if we compose a morphism with label x^{-1} y with a morphism with label y^{-1} z we get a morphism with label x^{-1} z = (x^{-1} y) (y^{-1} z), so labels multiply under composition

[Reid Barton]

So if we form the quotient EG/G, we get the category BG with one object and one morphism for each element of G, where composition of morphisms corresponds to multiplication in G.

[Reid Barton]

Now, let's look at simplices of the nerve of EG. An n-simplex of the nerve of EG is a functor from [n] = the category {0 -> 1 -> ... -> n} to EG.

[Reid Barton]

But in EG there's a unique morphism between any two objects, so this is just given by a function from {0, 1, ..., n} to G.

[Reid Barton]

The image of this simplex under the projection EG -> BG is now a functor from [n] to BG. In BG, there is just one object so the only interesting information is where the n morphisms 0 -> 1, 1 -> 2, ..., (n-1) -> n go. For each one I have to give an element of G.

[Reid Barton]

If my original simplex was described by (x_0, ..., x_n) then its image in BG is described by (x_0^{-1} x_1, ..., x_{n-1}^{-1} x_n).

[Reid Barton]

In the other direction, if I have a simplex in BG (g_1, ..., g_n), then one of the simplices that it is the image of is (1, g_1, g_1 g_2, g_1 g_2 g_3, ..., g_1 ... g_n), and the others are given by left multiplication by any g in G.

[Reid Barton]

So that is where the formula you were asking about comes from.

[Kevin Buzzard]

I'll need some time to digest this, but thanks (I'm trying to do some topology)

[Reid Barton]

If M has trivial G-action, then H^*(G, M) is the cohomology of this simplicial set BG = EG/G with coefficients in M. The complex that computes this has C^n = functions from n-simplices of EG/G to M, or from n-simplices of BG to M. Correspondingly this gives functions defined on (fin (n+1) -> G) / G or fin n -> G, with the above rule for translating between these representations. In this case, because M has trivial action, the former can also be thought of as G-equivariant functions from fin (n+1) -> G to M.
If M has nontrivial G-action, then I guess you need to say something about local systems and it's not quite as easy to relate group cohomology to simplicial cohomology.

[Reid Barton]

For the purpose of formalization, the EG description makes it trivial to show that you've got a simplicial set. The simplicial structure maps are just given by composing fin (m + 1) -> fin (n + 1) -> G

[Johan Commelin]

I've been meaning to return to the simplicial stuff for quite a while. But there are too many other things on my todo list... and it will require some coordination to get a flexible API.

[Ulrik Buchholtz]

Sorry to hijack your thread, but I've been meaning to do (or get a student to do) some group cohomology in HoTT, but I'm not exactly sure which theorems to aim for. I guess as a start, I'd prove that the two descriptions, in terms of homotopy theory (cohomology of BG with coefficients in M : BG -> Ab) and combinatorics (cohomology of some cochain complex), are equal. What would be a good test after that do you think?

[Kevin Buzzard]

I was not going to do anything topological (reflecting my background I guess). My plan was: (1) definition of $H^n(G,M)$ (2) proof that it's a functor from $G$-modules to abelian groups (3) long exact sequence of group cohomology (4) [probably won't get there] spectral sequence (5) [probably won't get there] some sort of uniqueness statement -- it's some universal delta-functor.

[Ulrik Buchholtz]

OK, thanks. Because we already have the long exact sequence and Serre spectral sequence in the HoTT libraries, we'd get the LES (3) and L-H-S spectral sequence (4) (sans multiplicative structure) for group cohomology as corollaries. I don't know if (5) would follow as well – maybe that would require a theory of module spectra (which we don't know how to do)?

[Kevin Buzzard]

You don't have the Serre spectral sequence for "honest topological spaces" though, just for these homotopy types. I would like to see an honest group cohomology spectral sequence in a HoTT theory, that would be great!

[Ulrik Buchholtz]

But homotopy types are precisely enough to talk about BG for any group G, etc., so I don't see what would be dishonest about the resulting group cohomology spectral sequence?

[Ulrik Buchholtz]

I'll see if I can put that together for our joint paper on the spectral sequence (which is way overdue)

[Reid Barton]

Sorry to hijack your thread, but I've been meaning to do (or get a student to do) some group cohomology in HoTT, but I'm not exactly sure which theorems to aim for. I guess as a start, I'd prove that the two descriptions, in terms of homotopy theory (cohomology of BG with coefficients in M : BG -> Ab) and combinatorics (cohomology of some cochain complex), are equal.

This already sounds quite challenging to me, or at least the method I would apply in "ordinary math" doesn't seem to work, because you can't build the geometric realization of a simplicial set in HoTT, can you?

[Reid Barton]

Oh right, you're the author of the $$\mathbb{RP}^n$ paper. Then I would believe you know how to do this, even though I don't.

[Reid Barton]

How about calculating the cohomology of free groups. That should be easier than Kevin's way :)

[Reid Barton]

Can I hijack your hijack and ask whether we know how to construct $BU$ in HoTT yet?

[Ulrik Buchholtz]

Can I hijack your hijack and ask whether we know how to construct $BU$ in HoTT yet?

I think so: construct $KU$ using Snaith's theorem, and take the connected component at the basepoint of $\mathbb{Z} \times BU \simeq \Omega^\infty KU$.

[Reid Barton]

Oh hmm

[Ulrik Buchholtz]

That still doesn't get us $BU(n)$, though, AFAICT.

[Ulrik Buchholtz]

This already sounds quite challenging to me, or at least the method I would apply in "ordinary math" doesn't seem to work, because you can't build the geometric realization of a simplicial set in HoTT, can you?

Right, we don't have geometric realization of simplicial sets, but here we can build a corresponding CW structure directly, I think, and we know (and have formalized in the Agda library) that the cellular cochain complex computes cohomology correctly.

[Kevin Buzzard]

But homotopy types are precisely enough to talk about BG for any group G, etc

Yes exactly! That's why I think this would be a brilliant thing to do in HoTT.