G-modules

Stream: maths

[Kevin Buzzard]

Today an undergraduate computer scientist and I are starting on group cohomology.

If $G$ is a group then a $G$-module $M$ is an abelian group equipped with an action of $G$ satisfying some axioms. There is some way of building a "group ring" $\mathbb{Z}[G]$ such that to give a $G$-module is equivalent to giving a module over the ring $\mathbb{Z}[G]$. Note that this ring is not commutative, so there is probably not much support for it in mathlib.

We need to make some design decisions about bundling and what have you. Does anyone have any recommendations? Following modules over a commutative ring we would be led to (M : Type*) [add_comm_group M] [G_module G M]. We will want to consider submodules and quotient modules, morphisms between these modules, kernels and cokernels of these morphisms, and exact sequences.

@Chris Hughes @Kenny Lau @Johan Commelin you guys have thought about modelling algebraic objects analogous to these in Lean before. Do any of you have any comments before we launch in?

[Johan Commelin]

Hmm... the group ring is already defined. That was one of the things we discovered during Lean Together.

[Johan Commelin]

I think that it might be easier to just use modules over the group ring

[Johan Commelin]

You say there is not much support. But there will definitely be a whole lot more support then \varnothing, which is the support you currently have for a G_module definition that start from scratch

[Kevin Buzzard]

What concerns me about this approach is that the student has no idea what a module over a ring is, and will want to write everything in the language of cocycles.