Zulip Chat Archive

Stream: general

Topic: group ring


view this post on Zulip Kenny Lau (Mar 29 2018 at 10:16):

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

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 10:20):

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

view this post on Zulip Kenny Lau (Mar 29 2018 at 10:20):

right

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 10:20):

which might be a bit icky

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 10:20):

induction on size of support?

view this post on Zulip Kenny Lau (Mar 29 2018 at 10:20):

well we have the master of finite sums

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 10:20):

he's revising mechanics

view this post on Zulip Kenny Lau (Mar 29 2018 at 10:20):

...

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 10:22):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johannes Hölzl (Mar 29 2018 at 10:34):

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

view this post on Zulip 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'

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 11:57):

At first glance this looks like exactly the right thing

view this post on Zulip 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.

view this post on Zulip 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: May 06 2021 at 21:09 UTC