Zulip Chat Archive

Stream: maths

Topic: distrib -- I take it all back


view this post on Zulip Kevin Buzzard (Mar 09 2021 at 19:09):

I am preparing my lectures on group cohomology. This is the third time that I have thought seriously about the subject, and, just like schemes, the more I think about it using Lean and the more I re-investigate the idea, the better I understand it. I think that Patrick had a similar experience with his understanding of topology and its relationship to the theory of filters, Patrick's explanation of the theory of topological spaces, uniform spaces and filters ended up being better than Bourbaki's (for example Bourbaki got the definition wrong -- this was proved by people like I. James and formalised by people like @Johannes Hölzl . Patrick understood that topological spaces are just a special case of filters, they're neighbourhood filters, that's why filters are a really cool way to do topology.

So similarly, I am thinking today about the theory of G-modules, where G is a group and M is an abelian group, because this is the important case which has got a lot of mileage in mathematics where we're interested in the Langlands philosophy and don't give a monkeys about stupid things like groups with zero and distribs.

So I was very privileged to work with two Imperial students @Anca Ciobanu and @Shenyang Wu . Anca formalised the theory of group cohomology in low degree in her project here and Shenyang has definitions of nn-cycles and nn-coboundaries and a theory of general group cohomology here. Thanks to Patrick Massot, you can just use leanproject get to pull these working repositories onto your computer, and while they won't be compatible with modern mathlib you can just clone them and play with them as one-off repos or refactor them or abstract out some API and PR a version which compiles with mathlib master (there are no guarantees that any of my students projects compile with master, they are stand-alone pieces but can certainly be regarded as a guide to an API for the area they cover.

So I'm formalising the theory of H0H^0 and when I'm trying to get the definitions working in full generality, like one is supposed to do in mathlib, I realise that the structures I need are variables {G M : Type} [monoid G] [add_comm_group M] [distrib_mul_action G M]. I could let M be an add_comm_monoid but you need groups to say almost anything interesting and it was annoying that there's two kernels in the theory of morphisms -- a monoid kernel and a group kernel -- so I just switched to add_comm_group. So I've never seen this distrib_mul_action G M before, for all I know it was invented by Kenny or Eric or one of these people who knows a lot about this kind of machinery, so I took a look at it and it's just two axioms and they made me laugh :-)

The first is smul_zero, which says r • 0 = 0 and which looks really similar to Johan's monoid_with_zero, an abstraction we are putting to good use in the application to groups with zero in valuation theory (we needed these for perfectoid spaces). And the second is smul_add : r • (x + y) = r • x + r • y which is just another distrib! Is H0H^0 in some weird way the theory of distribs? Is a commutative ring just a special case of a distrib_mul_action when G and M are the same type? "Let a monoid RR act on the same abelian group RR". That's a commutative ring.

I have a lot more to say about this but I thought that this was a good place to start :-)

view this post on Zulip Damiano Testa (Mar 09 2021 at 19:22):

Kevin, maybe I am confused, but there seems to be an asymmetry between left and right in this example: do you need to assume that (_ + _) \smul _ distributes as well? Commutativity might do this for you, but you seem to be multiplying only from the left. Is there an axiom that smul commutes?
(I meant, to get a ring out of this!)

view this post on Zulip Eric Wieser (Mar 09 2021 at 19:28):

Right, the missing lemmas about distributivity on the right are added by semimodule

view this post on Zulip Eric Wieser (Mar 09 2021 at 19:29):

docs#semiring.to_semimodule is your "a (commutative) (semi)ring is a mul_action"

view this post on Zulip Eric Wieser (Mar 09 2021 at 19:31):

(deleted)

view this post on Zulip Adam Topaz (Mar 09 2021 at 19:32):

@Kevin Buzzard How far down the rabbit hole do you want to go? H^0 is the global sections of an abelian sheaf on the classifying site of the monoid

view this post on Zulip Kevin Buzzard (Mar 09 2021 at 22:21):

There might be several different models of H0H^0. The explicit approach via nn-cocycles was historically useful, and back then it was possible to check your signs. Then Grothendieck came along and proposed that cohomology be defined by a slightly subtle universal property which demands not only groups Hn(G,M)H^n(G,M) but an explicit choice of connecting homomorphisms Hn(C)Hn+1(A)H^n(C)\to H^{n+1}(A), examples of which are in the literature for the explicit model of HnH^n as cocycles over coboundaries, but it would be interesting to know if they all coincided with each other.

Adam I think that my way of thinking about it is more down-to-earth, you're using that sheaves are representations of fundamental groups and the fact that you can make some kind of equivalence class of topological spaces which have a given monoid as fundamental monoid. To what extent is your topological space or site or whatever it is well-defined? Up to isomorphism or a weaker equivalence? How am I supposed to understand your definition?

view this post on Zulip Adam Topaz (Mar 09 2021 at 22:22):

I'm just thinking of the category of G-sets (just like in the case where G is a group) where covers are jointly surjective families of morphisms

view this post on Zulip Adam Topaz (Mar 09 2021 at 22:23):

I'm fairly certain that the global sections then agrees with the G-invariants, so by general nonsense about derived functors, you should get the right answer.

view this post on Zulip Adam Topaz (Mar 09 2021 at 22:24):

And besides, if the global sections do not agree with the G-invariants, then maybe the G-invariants is not the right object to begin with

view this post on Zulip Kevin Buzzard (Mar 09 2021 at 22:24):

The general nonsense about derived functors does not give you explicit identifications between the abstractly defined cohomology groups and the concrete model as cocycles over coboundaries

view this post on Zulip Adam Topaz (Mar 09 2021 at 22:25):

Of course youre right, you need to find the correct free resolution of Z\mathbb{Z} as a Z[G]\mathbb{Z}[G]-module

view this post on Zulip Adam Topaz (Mar 09 2021 at 22:26):

So I guess you can define these cohomology groups as ExtZ[G]i(Z,M)\mathrm{Ext}^i_{\mathbb{Z}[G]}(\mathbb{Z},M).

view this post on Zulip Kevin Buzzard (Mar 10 2021 at 07:20):

The switch from the standard resolution to the bar resolution (I hope I've got these names right) makes essential use of the fact that M is an abelian group rather than just an abelian monoid

view this post on Zulip Kevin Buzzard (Mar 10 2021 at 07:22):

Another difference is that a sheaf on the category of G-sets is at the end of the day a lot more raw data than a distrib_mul_action of a group on an abelian group.

view this post on Zulip Patrick Massot (Mar 10 2021 at 08:33):

Kevin Buzzard said:

I think that Patrick had a similar experience with his understanding of topology and its relationship to the theory of filters, Patrick's explanation of the theory of topological spaces, uniform spaces and filters ended up being better than Bourbaki's (for example Bourbaki got the definition wrong -- this was proved by people like I. James and formalised by people like @Johannes Hölzl .

I. James uses the same definition as Bourbaki. Johannes wasn't the first one to introduce the definition we use (the Wikipedia page says there are two competing definitions). And of course saying Bourbaki has the wrong one is debatable. The definition we use is certainly much easier for formalization, but it does requires adding properness assumptions in lots of lemmas. So I still think we have the right definition but Bourbaki's one is not wrong.

view this post on Zulip Patrick Massot (Mar 10 2021 at 08:45):

Patrick understood that topological spaces are just a special case of filters, they're neighbourhood filters, that's why filters are a really cool way to do topology.

I'm not sure what this sentence means but everything possible meaning makes it wrong.

view this post on Zulip Patrick Massot (Mar 10 2021 at 08:46):

We did contribute things, this is all described in the perfectoid paper. The main thing is a better extension by continuity theorem. Bourbaki's version is not general enough and this defect complicates things in several places later in the book.

view this post on Zulip Patrick Massot (Mar 10 2021 at 08:47):

A less important point is that Bourbaki's version of this very important theorem is also wrong, but this is a typo. They are missing an assumption, and it doesn't show up in the proof because this part of the proof is left to readers.

view this post on Zulip Patrick Massot (Mar 10 2021 at 08:49):

There is also a proof about uniform spaces that is completely wrong in Bourbaki, and copied word by word in James' book. But I guess this was noticed before and fixed in another book. This is a very easy lemma, not at all the same depth as the extension theorem, I have no idea what happened.

view this post on Zulip Adam Topaz (Mar 10 2021 at 14:22):

Kevin Buzzard said:

The switch from the standard resolution to the bar resolution (I hope I've got these names right) makes essential use of the fact that M is an abelian group rather than just an abelian monoid

I must have misunderstood. I thought you wanted to take M to be an abelian group and G a monoid acting on M.

view this post on Zulip Kevin Buzzard (Mar 11 2021 at 07:37):

Yes that's absolutely right, I am just now rather tuned to all the places where subtraction is used :-) The other place it's used is in the coboundary map sending a 0-cochain m to the 1-cochain sending g to gm-m or m-gm.


Last updated: May 06 2021 at 18:20 UTC