group with two elements

Stream: Is there code for X?

[Yury G. Kudryashov]

Hi, do we have a canonical multiplicative group with 2 elements? Extra points for a group that works well with @[to_additive].

[Eric Rodriguez]

I mean, sort of by the by but does multiplicative G actually additivise properly?

[Yury G. Kudryashov]

Last time I checked, it didn't.

[Yury G. Kudryashov]

But @[to_additive] becomes more powerful once in a while.

[Eric Rodriguez]

I guess you could use the dihedral group of 1? Or maybe units of zmod 3

[Eric Rodriguez]

But none of those additivise well

[Yury G. Kudryashov]

Or multiplicative (fin 2) = multiplicative (zmod 2).

[Eric Rodriguez]

I thought that option was ugly, but it will work better if to_additive is improved to use it

[Yury G. Kudryashov]

I can use any ugly option with local notation. Though I won't be able to define

def my_fun : G → G
| 1 := _
| σ := _

[Heather Macbeth]

There is ![_, _] to write a function from multiplicative (fin 2) or multiplicative (zmod 2) (as you probably know).

[Kevin Buzzard]

When María Inés needed the multiplicative infinite cyclic group she just used multiplicative int.

[Anatole Dedecker]

This won’t additivize well, but you could use units int (this is the return type of docs#equiv.perm.sign for example)

[Heather Macbeth]

Related, @Alex Kontorovich asked me if there could be a way to simply designate one group as the to_additive of another. I'm currently redoing Fourier theory on the additive circle (branch#fourier-add-circle) and it's nearly an exact copy of Fourier theory on the multiplicative circle.

[Jireh Loreaux]

I guess this would need some choice of isomorphism though, right? I don't think to_additive has any kind of support for that. I guess there's only one continuous one in this case, but lots of discontinuous ones. What exactly would you want this designation to do?