Zulip Chat Archive

Stream: general

Topic: general sign function

Eric Rodriguez (Mar 07 2022 at 17:36):

have we there been discussion about making sign(x) for x as general as possible? something like this:

def sign {α} [has_lt α] [has_zero α] [decidable_rel ((<) : α → α → Prop)] (a : α) :=
if 0 < a then (1 : ℤ) else if a < 0 then -1 else 0

I'm not too sure what's of more general use - for one, should we use 1/-1 in the type itself? then we need has_neg and has_one, that's something fairly big; we can always use zsmul, but that can be inconvenient. plus, is this the right way to state it for non total orders? do we care about what happens on partial orders at all?

Bolton Bailey (Mar 08 2022 at 02:13):

A version more general for some purposes but less for others would be x/abs(x). This would include phase for complex numbers.

Martin Dvořák (Mar 08 2022 at 18:11):

Which would also work for zero, wouldn't it?

Eric Wieser (Mar 08 2022 at 18:24):

Is unitary α a silly return type for this? (docs#unitary)

Kevin Buzzard (Mar 08 2022 at 18:38):

I think sign(0)=0 :-/

Adam Topaz (Mar 08 2022 at 18:55):

What's the problem with sign(0) = 0? This is the only way for sign to be a morphism of hyperrings.

Yakov Pechersky (Mar 08 2022 at 19:07):

Codomain of sign as with_zero (units int)?

Adam Topaz (Mar 08 2022 at 19:07):

Yeah, something like that.

Adam Topaz (Mar 08 2022 at 19:08):

~~Or with_zero (roots_of_unity 2) if we have roots_of_unity ???~~
Bah, it seems that we don't have $\mu_n$ as a type by itself (as opposed to a subgroup of the units of a monoid)

Eric Wieser (Mar 08 2022 at 19:11):

Isn't "roots of unity" close enough to unitary?

Adam Topaz (Mar 08 2022 at 19:13):

I'm not sure what you mean? Unitary as in docs#unitary ?

Eric Wieser (Mar 08 2022 at 19:15):

Yes, but admittedly I'm only thinking about the reals, complex numbers, and quarternions

Adam Topaz (Mar 08 2022 at 19:17):

In $\mathbb{C}$ , if $|z| = 1$ then $z$ is unitary, but that would include many things that are not roots of unity!

Adam Topaz (Mar 08 2022 at 19:18):

We do have docs#roots_of_unity

Adam Topaz (Mar 08 2022 at 19:20):

But in informal math there is a bit of overloading of notation: $\mu_n$ can refer to "the" group of roots of $n$-th roots of unity, which is just a (multiplicative) cyclic group of order $n$ , or it could refer to the functor taking a commutative monoid $M$ (well, usually a ring $A$ ) to $\mu_n(M)$ which is the set of all $m \in M$ satisfying $m^n = 1$ .

Eric Wieser (Mar 08 2022 at 19:21):

Ah, then I got confused by your suggestion, which isn't compatible with the suggestion above of having sign (z : ℂ) morally equal to z / |z|

Adam Topaz (Mar 08 2022 at 19:23):

Ah! I see what you mean. Yes, this is the right approach for sure!
If you take the unit circle in $\mathbb{C}$ and add $0$ , this is a multiplicative monoid, and you can give it one of the so-called hyperring structures making that sign function into a morphism of hyperrings.

Eric Wieser (Mar 08 2022 at 19:23):

Is hyperring something mathlib knows about?

Adam Topaz (Mar 08 2022 at 19:24):

see page 2 of https://arxiv.org/pdf/1601.01204.pdf (hyperfield of phases)

Adam Topaz (Mar 08 2022 at 19:25):

Eric Wieser said:

Is hyperring something mathlib knows about?

No, but maybe it should. And I have some ideas for how one might do this.

Last updated: Dec 20 2023 at 11:08 UTC