Zulip Chat Archive

Stream: maths

Topic: group cohomology


view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 07 2019 at 21:51):

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

view this post on Zulip Kevin Buzzard (Nov 07 2019 at 21:52):

Thanks.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 07 2019 at 21:55):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 07 2019 at 21:58):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Nov 07 2019 at 22:00):

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

view this post on Zulip Reid Barton (Nov 07 2019 at 22:01):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Nov 07 2019 at 22:02):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 07 2019 at 22:02):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 07 2019 at 22:04):

but then you have to work around this quotient issue

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 07 2019 at 22:05):

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

view this post on Zulip Reid Barton (Nov 07 2019 at 22:06):

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

view this post on Zulip Reid Barton (Nov 07 2019 at 22:06):

when M has nontrivial action

view this post on Zulip Reid Barton (Nov 07 2019 at 22:06):

Oh, it's even in your question.

view this post on Zulip Kevin Buzzard (Nov 07 2019 at 22:07):

I should probably read that question at some point

view this post on Zulip Reid Barton (Nov 07 2019 at 22:10):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Nov 07 2019 at 22:11):

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

view this post on Zulip Kevin Buzzard (Nov 07 2019 at 22:11):

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

view this post on Zulip Reid Barton (Nov 07 2019 at 22:14):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 07 2019 at 22:17):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Reid Barton (Nov 07 2019 at 22:24):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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 Hn(G,M)H^n(G,M) (2) proof that it's a functor from GG-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.

view this post on Zulip 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)?

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Reid Barton (Nov 08 2019 at 14:01):

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

view this post on Zulip Reid Barton (Nov 08 2019 at 14:04):

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

view this post on Zulip Ulrik Buchholtz (Nov 08 2019 at 14:09):

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

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

view this post on Zulip Reid Barton (Nov 08 2019 at 14:10):

Oh hmm

view this post on Zulip Ulrik Buchholtz (Nov 08 2019 at 14:11):

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

view this post on Zulip 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.

view this post on Zulip 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