Zulip Chat Archive

Stream: general

Topic: group ring


Kenny Lau (Mar 29 2018 at 10:16):

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

Kevin Buzzard (Mar 29 2018 at 10:20):

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

Kenny Lau (Mar 29 2018 at 10:20):

right

Kevin Buzzard (Mar 29 2018 at 10:20):

which might be a bit icky

Kevin Buzzard (Mar 29 2018 at 10:20):

induction on size of support?

Kenny Lau (Mar 29 2018 at 10:20):

well we have the master of finite sums

Kevin Buzzard (Mar 29 2018 at 10:20):

he's revising mechanics

Kenny Lau (Mar 29 2018 at 10:20):

...

Kevin Buzzard (Mar 29 2018 at 10:22):

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 (Mar 29 2018 at 10:22):

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

Kevin Buzzard (Mar 29 2018 at 10:28):

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 (Mar 29 2018 at 10:28):

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 (Mar 29 2018 at 10:32):

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 (Mar 29 2018 at 10:34):

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

Johannes Hölzl (Mar 29 2018 at 10:44):

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 (Mar 29 2018 at 11:57):

At first glance this looks like exactly the right thing

Kevin Buzzard (Mar 29 2018 at 11:57):

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

Kevin Buzzard (Mar 29 2018 at 11:58):

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


Last updated: Dec 20 2023 at 11:08 UTC