Zulip Chat Archive

Stream: maths

Topic: gpowers


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?

Scott Morrison (Jul 24 2020 at 12:32):

Yeah, gpowers should certainly be the subgroup.

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)

Kevin Buzzard (Jul 24 2020 at 14:23):

I see!

Chris Hughes (Jul 24 2020 at 15:55):

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

Kevin Buzzard (Jul 24 2020 at 16:54):

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

Yury G. Kudryashov (Jul 24 2020 at 19:56):

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

Yury G. Kudryashov (Jul 24 2020 at 19:57):

So we can go with mem_closure_singleton instead of introducing gpowers.

Yury G. Kudryashov (Jul 24 2020 at 19:57):

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

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: Dec 20 2023 at 11:08 UTC