complex.has_scalar

Stream: maths

[Yury G. Kudryashov]

I've just noticed that any type that acts on $\mathbb R$ automatically acts on $\mathbb C$, thanks to docs#complex.has_scalar. Do we actually use it for $R \ne\mathbb R$?

[Yury G. Kudryashov]

One day we might want to add the action of (a type synonym for) multiplicative (zmod 2) or equiv.perm (fin 2) on is_R_or_C k by conj (or should I say star?). Then we'll have a diamond.

[Yaël Dillies]

Does that not create a problem with nsmul already?

[Yury G. Kudryashov]

Probably, it creates a non-defeq diamond for nsmul. The example above creates a diamond with no propositional equality.

[Sebastien Gouezel]

Isn't it defeq by design for nsmul?

[Eric Wieser]

It's useful for the action by nnreal I imagine

[Yury G. Kudryashov]

Sebastien Gouezel said:

Isn't it defeq by design for nsmul?

No, it is defeq by design for has_scalar ℝ ℂ. For has_scalar ℕ ℂ, one instance results in 1 • z = z + 0 while the other results in (1 : ℝ) • z.

[Yury G. Kudryashov]

Eric Wieser said:

It's useful for the action by nnreal I imagine

See docs#nnreal.mul_action

[Eric Wieser]

Are you sure your claim about nsmul is true? I assume src#complex.comm_ring is where the implementation is

[Eric Wieser]

Indeed the implementation is

nsmul := λ n z, ⟨n • z.re - 0 * z.im, n • z.im + 0 * z.re⟩,

Isn't that the same as src#complex.has_scalar?

[Yury G. Kudryashov]

You're right.

[Eric Wieser]

I think you end up with a diamond in general if you true to make a star action as you suggest though

[Eric Wieser]

Consider the action on complex matrices, where one path to the diamond transposes but the other doesn't

[Yury G. Kudryashov]

@Sebastien Gouezel Do we ever need this transitive instance?

[Eric Wieser]

One way to solve this might be a allow_transitive_smul typeclass, which has to be present to enable transitivity; it would be skipped for the conj action you mention

[Eric Wieser]

I think I'm actually the one responsible for that transitive instance

[Yury G. Kudryashov]

I think that before discussing workarounds we should figure out whether we need it.

[Eric Wieser]

My point with my comment above is that the instance you're proposing causes problems elsewhere too, not just on the complex numbers. So I'd argue that complex.has_scalar is not really the problem, the problem is the new instance you propose.

[Yury G. Kudryashov]

Could you please elaborate? What action on matrices are you talking about?

[Eric Wieser]

The same one by multiplicative (zmod 2) as you mention, presumably where of_add 1 • M is conj M/ star M and of_add 0 • M = M

[Eric Wieser]

(assuming I read your message correctly)

[Eric Wieser]

Which isn't to say I think your instance is a bad idea in isolation, but that complex.has_scalar forming a diamond with it is a symptom of a bigger problem with actions as a whole.

[Sebastien Gouezel]

Yury G. Kudryashov said:

Sebastien Gouezel Do we ever need this transitive instance?

Personally I never needed it, no, and I agree I don't really see in which situation it would be useful.

[Eric Wieser]

I think the case I was thinking of was cases when R is nothing concrete, and instead of requiring separate actions on R and C that agree ([has_scalar R ℝ] [has_scalar R ℂ] [is_scalar_tower R ℝ ℂ]), you can just assume [has_scalar R ℝ] and get the other action for free.

[Eric Wieser]

In the same way that instead of writing [has_scalar R ℝ] [has_scalar R (ι → ℝ)] [is_scalar_tower R ℝ (ι → ℝ)] we can currently write [has_scalar R ℝ] and get the pi action for free.

[Sebastien Gouezel]

But is there a situation where it is useful to state or prove a genuine theorem? There are many actions that we could declare, but that we probably shouldn't declare globally if they are not useful enough. I am wondering if we are in this situation, or if there is a convincing example that it is a good idea to have it.

[Yury G. Kudryashov]

And we possibly have a diamond because of docs#rat.algebra_rat

[Eric Wieser]

That diamond is all over the place though, so I don't think is really relevant to this discussion

[Eric Wieser]

Sebastien Gouezel said:

But is there a situation where it is useful to state or prove a genuine theorem? There are many actions that we could declare, but that we probably shouldn't declare globally if they are not useful enough. I am wondering if we are in this situation, or if there is a convincing example that it is a good idea to have it.

I'm not really opposed to changing it to a def that's locally an instance for the few lemmas about it today; that way if we need it back again, it's easy to re-enable without rebuilding everything

[Yury G. Kudryashov]

Eric Wieser said:

That diamond is all over the place though, so I don't think is really relevant to this discussion

Is it? Do we have lots of instances that result in a different $\mathbb Q$-action?

[Eric Wieser]

Hmm, maybe you're right. I guess there aren't many fields that are constructed directly out of smaller fields

[Eric Wieser]

Maybe the action on subfields also has such a diamond? I haven't checked.