Zulip Chat Archive

Stream: maths

Topic: to_additive, gpow, smul


view this post on Zulip Patrick Massot (Oct 01 2020 at 15:43):

In this comment Sébastien naturally asks about deducing a lemma in additive group theory from the corresponding one for multiplicative groups. The reason we didn't do that is that to_additive currently doesn't handle translation of gpow which allows to write gng^n for gg in a multiplicative group and nn is an integer into the additive version gsmul allowing to write ngng where gg now belongs to an additive group. The definition is:

def gsmul (n : ) (a : A) : A :=
@gpow (multiplicative A) _ a n

I guess this has been discussed before. Is it hopelessly out of scope for to_additive? Is there a reason not to want to_addtive to handle this? Or is it only that someone needs to go and add to_additive everywhere?

view this post on Zulip Kevin Buzzard (Oct 01 2020 at 17:19):

The issue is that the order of the variables changes

view this post on Zulip Kevin Buzzard (Oct 01 2020 at 17:19):

and right now that isn't supported

view this post on Zulip Kevin Buzzard (Oct 01 2020 at 17:20):

Maybe we could have [reducible] gsmul_aux a n := gsmul n a and then get it all working for aux and then just live with the corresponding reducible annoyance which presumably be like in the ge days

view this post on Zulip Kevin Buzzard (Oct 01 2020 at 17:21):

I don't know if to_additive could eat an abbreviation but maybe if it could then that would work better

view this post on Zulip Reid Barton (Oct 01 2020 at 17:25):

The lemma names also tend to have a corresponding permutation applied to their components, which might be tough for to_additive to replicate

view this post on Zulip Yury G. Kudryashov (Oct 01 2020 at 17:54):

And lemma arguments often come in different order.

view this post on Zulip Yury G. Kudryashov (Oct 01 2020 at 17:55):

Currently the standard way to get from pow/gpow to nsmul/gsmul is to apply the original lemma to @multiplicative α.

view this post on Zulip Kevin Buzzard (Oct 01 2020 at 18:01):

@Jason KY. I made you an unwitting recipient of an experiment with this. When we were setting up group theory from first principles I defined {{n}}^g to mean g^n because I wanted to see if anything felt more natural that way around. But I think it just ended up annoying you, right?

view this post on Zulip Kevin Buzzard (Oct 01 2020 at 18:01):

We could make Zsmul a right action?

view this post on Zulip Kevin Buzzard (Oct 01 2020 at 18:02):

It's not the same as smul, after all

view this post on Zulip Patrick Massot (Oct 01 2020 at 18:43):

@Sebastien Gouezel do you agree this all mean we should merge the subgroup PR without trying to fix this to_additive issue?

view this post on Zulip Jason KY. (Oct 01 2020 at 19:50):

Kevin Buzzard said:

Jason KY. I made you an unwitting recipient of an experiment with this. When we were setting up group theory from first principles I defined {{n}}^g to mean g^n because I wanted to see if anything felt more natural that way around. But I think it just ended up annoying you, right?

I didn't find the direction of the g and n to be annoying but the fact that I had to write the squiggly brackets every time!

view this post on Zulip Sebastien Gouezel (Oct 01 2020 at 20:07):

Yes, sure!


Last updated: May 06 2021 at 17:38 UTC