# Zulip Chat Archive

## Stream: maths

### Topic: group cohomology

#### Kevin Buzzard (Nov 07 2019 at 12:24):

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 (Nov 07 2019 at 21:51):

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

#### Kevin Buzzard (Nov 07 2019 at 21:51):

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 (Nov 07 2019 at 21:51):

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

#### Reid Barton (Nov 07 2019 at 21:51):

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

#### Kevin Buzzard (Nov 07 2019 at 21:52):

Thanks.

#### Reid Barton (Nov 07 2019 at 21:52):

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 (Nov 07 2019 at 21:53):

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 (Nov 07 2019 at 21:55):

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

#### Reid Barton (Nov 07 2019 at 21:57):

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

#### Kevin Buzzard (Nov 07 2019 at 21:58):

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

#### Kevin Buzzard (Nov 07 2019 at 21:59):

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 (Nov 07 2019 at 22:00):

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

#### Reid Barton (Nov 07 2019 at 22:01):

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

#### Reid Barton (Nov 07 2019 at 22:01):

In your second setup, are you planning to mod out `fin (n + 1) -> G`

by the diagonal action of G?

#### Kevin Buzzard (Nov 07 2019 at 22:02):

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

#### Reid Barton (Nov 07 2019 at 22:02):

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 (Nov 07 2019 at 22:02):

#### Kevin Buzzard (Nov 07 2019 at 22:03):

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 (Nov 07 2019 at 22:03):

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 (Nov 07 2019 at 22:04):

but then you have to work around this quotient issue

#### Reid Barton (Nov 07 2019 at 22:05):

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 (Nov 07 2019 at 22:05):

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

to `M`

#### Reid Barton (Nov 07 2019 at 22:06):

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

#### Reid Barton (Nov 07 2019 at 22:06):

when M has nontrivial action

#### Reid Barton (Nov 07 2019 at 22:06):

Oh, it's even in your question.

#### Kevin Buzzard (Nov 07 2019 at 22:07):

I should probably read that question at some point

#### Reid Barton (Nov 07 2019 at 22:10):

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

#### Kevin Buzzard (Nov 07 2019 at 22:10):

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

#### Reid Barton (Nov 07 2019 at 22:11):

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

#### Kevin Buzzard (Nov 07 2019 at 22:11):

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

#### Reid Barton (Nov 07 2019 at 22:14):

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

#### Reid Barton (Nov 07 2019 at 22:14):

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 (Nov 07 2019 at 22:16):

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 (Nov 07 2019 at 22:17):

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

#### Reid Barton (Nov 07 2019 at 22:19):

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 (Nov 07 2019 at 22:20):

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 (Nov 07 2019 at 22:20):

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 (Nov 07 2019 at 22:21):

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 (Nov 07 2019 at 22:21):

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 (Nov 07 2019 at 22:22):

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 (Nov 07 2019 at 22:23):

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 (Nov 07 2019 at 22:24):

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 (Nov 07 2019 at 22:24):

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

#### Kevin Buzzard (Nov 07 2019 at 22:25):

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

#### Reid Barton (Nov 07 2019 at 22:32):

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 (Nov 07 2019 at 22:34):

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 (Nov 08 2019 at 06:41):

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 (Nov 08 2019 at 10:59):

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 (Nov 08 2019 at 11:39):

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 (Nov 08 2019 at 11:53):

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 (Nov 08 2019 at 11:56):

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 (Nov 08 2019 at 12:01):

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 (Nov 08 2019 at 12:02):

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

#### Reid Barton (Nov 08 2019 at 13:18):

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 (Nov 08 2019 at 14:01):

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 (Nov 08 2019 at 14:01):

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

#### Reid Barton (Nov 08 2019 at 14:04):

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

#### Ulrik Buchholtz (Nov 08 2019 at 14:09):

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 (Nov 08 2019 at 14:10):

Oh hmm

#### Ulrik Buchholtz (Nov 08 2019 at 14:11):

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

#### Ulrik Buchholtz (Nov 08 2019 at 14:14):

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 (Nov 08 2019 at 15:10):

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.

Last updated: May 18 2021 at 08:14 UTC