gpowers

Stream: maths

[Kevin Buzzard]

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]

Yeah, gpowers should certainly be the subgroup.

[Mario Carneiro]

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

[Kevin Buzzard]

I see!

[Chris Hughes]

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

[Kevin Buzzard]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

So we can go with mem_closure_singleton instead of introducing gpowers.

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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