Zulip Chat Archive

Stream: maths

Topic: gpowers


view this post on Zulip Kevin Buzzard (Jul 24 2020 at 12:28):

Currently if g is in a group, gpowers g is the subset {gpow g n | n : int} and it's a theorem that this is a is_subgroup. I'm removing is_subgroup from mathlib in a branch (and it's really good fun, it's got to the point where most of the refactoring is high-powered stuff and it's fun to fix the proofs). I tried replacing gpowers g with the subgroup closure of the singleton g, but the underlying set is now not defeq to the g^n and I'm constantly having to rewrite. How about I rename gpowers (the subgroup generated by g as a set) to gpowers.carrier and redefine gpowers g to be the subgroup, with carrier defeq to the powers of g? Is the set really more important than the subgroup?

view this post on Zulip Scott Morrison (Jul 24 2020 at 12:32):

Yeah, gpowers should certainly be the subgroup.

view this post on Zulip Mario Carneiro (Jul 24 2020 at 12:58):

I don't think gpowers.carrier needs a name at all. Just call it (gpowers g : set g)

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 14:23):

I see!

view this post on Zulip Chris Hughes (Jul 24 2020 at 15:55):

I think I remember making subgroup.gpowers a while ago.

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 16:54):

I'll take a look. There's certainly an is_subgroup gpowers

view this post on Zulip Yury G. Kudryashov (Jul 24 2020 at 19:56):

Note that in linear algebra we just use span {x}.

view this post on Zulip Yury G. Kudryashov (Jul 24 2020 at 19:57):

So we can go with mem_closure_singleton instead of introducing gpowers.

view this post on Zulip Yury G. Kudryashov (Jul 24 2020 at 19:57):

(I don't remember how it is currently done for bundled submonoids and subgroups)

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 21:10):

For bundled submonoids I just added powers m and multiplies a. These things are perhaps much more useful in group theory than ring theory. The subgroup generated by an element is a fundamental construction in the theory of finite groups, but we don't usually analyse vector spaces by drawing lines in them


Last updated: May 12 2021 at 08:14 UTC