group ring

Stream: general

[Kenny Lau]

Do we have group rings? It's an instance of finsupp

[Kevin Buzzard]

so you just need to define the multiplication and then prove things like associativity

[Kenny Lau]

right

[Kevin Buzzard]

which might be a bit icky

[Kevin Buzzard]

induction on size of support?

[Kenny Lau]

well we have the master of finite sums

[Kevin Buzzard]

he's revising mechanics

[Kenny Lau]

...

[Kevin Buzzard]

For those who don't know the mathematics, if R is a commutative ring and G is a group (or even a monoid) then the group ring R[G] (or monoid ring) has as elements the finite formal combinations r1*g1+r2*g2+...+rn*gn

[Kevin Buzzard]

and multiplication is R-linear and extends the multiplication on the group.

[Kevin Buzzard]

There are a whole load of things which it would be natural and fun to do in Lean. We have modules over a ring, and tensor products, so if we have exact sequences then we could do Ext and Tor (projective and injective modules should be straightforward). If we also had group rings we could then do group cohomology. A lot of this is very dry homological algebra which should be very easy in Lean although there might be some foundational work to do to make diagram chases painless.

[Kevin Buzzard]

Kenny -- Sjoerd de Vries was talking about implementing group cohomology in Lean over the summer, so it's one of the things on my todo list for July, but if you want to start earlier then that's fine by me.

[Johannes Hölzl]

In https://github.com/leanprover/mathlib/blob/master/data/finsupp.lean#L646 is the following definition:
def to_ring [add_monoid α] [ring β] : ring (α →₀ β)
There is also a commutative version.

I didn't set it up as a type class instance as I think it is better to define a copy for this purpose.

[Johannes Hölzl]

Hm, actually I'm not sure if this is the one you are looking for ...

[Johannes Hölzl]

The problem is that to_ring is defined on the additive class for monoid and I guess you want to see it using the multiplicative structure. But otherwise it should work, it extends the multiplication in the group:

(r_1 * g_1 + \dots + r_n * g_n) * (1 * g') = r_1 * g_1g' + \dots + r_n * g_ng'

[Kevin Buzzard]

At first glance this looks like exactly the right thing

[Kevin Buzzard]

Yes, usually in maths the monoid is written multiplicatively, because the multiplication on the ring extends that on the monoid.

[Kevin Buzzard]

In fact I suspect that the monoid ring R[M] is probably some adjoint functor to the forgetful functor sending an R-algebra to the underlying multiplicative monoid