distrib -- I take it all back

Stream: maths

[Kevin Buzzard]

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 $H^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 $H^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 $R$ act on the same abelian group $R$". 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 :-)

[Damiano Testa]

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!)

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

(deleted)

[Adam Topaz]

@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

[Kevin Buzzard]

There might be several different models of $H^0$. The explicit approach via $n$-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 $H^n(G,M)$ but an explicit choice of connecting homomorphisms $H^n(C)\to H^{n+1}(A)$, examples of which are in the literature for the explicit model of $H^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?

[Adam Topaz]

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

[Adam Topaz]

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.

[Adam Topaz]

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

[Kevin Buzzard]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Patrick Massot]

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.

[Patrick Massot]

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.

[Patrick Massot]

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.

[Patrick Massot]

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.

[Patrick Massot]

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.

[Adam Topaz]

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.

[Kevin Buzzard]

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.