Zulip Chat Archive

Stream: maths

Topic: Group Algebras?


view this post on Zulip Thomas Browning (Dec 04 2020 at 01:25):

Does mathlib have group algebras yet (i.e., FG where F is a field and G is a finite group)? I can't find it mentioned in the usual places, but it seems like a sort of thing where a disguised version (i.e., a ring structure on functions from G to F) might be hidden somewhere.

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 01:26):

If G is finite it's just F -> G G -> F, so you could check to see if there's a ring structure on that if G is a fintype and a group, and F is a field (or a commutative ring).

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 01:26):

You could import all :-)

view this post on Zulip Kenny Lau (Dec 04 2020 at 01:26):

it's G \to\0 F (fin. supp. functions) right

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 01:26):

Oh I went the wrong way :D (I think it's time for bed)

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 01:27):

Yes, for general G you need finitely supported functions.

view this post on Zulip Adam Topaz (Dec 04 2020 at 01:34):

docs#monoid_algebra


Last updated: May 09 2021 at 11:09 UTC