Too many 'Smul's

Stream: mathlib4

[Michael Stoll]

I got the impression that there are too many different things that are all represented as • in Mathlib. Consider the following.

import Mathlib.Algebra.Polynomial.AlgebraMap

variable {R : Type*} [CommSemiring R]

open Polynomial

-- A perfectly good action of `R` on `R[X]`:
noncomputable
def act (r : R) (f : R[X]) : R[X] := aeval (C r * X) f

noncomputable
instance inst1 : MulSemiringAction R R[X] where
  smul r f := act r f
  one_smul f := by change act 1 f = f; simp [act]
  mul_smul r s f := by
    change act (r * s) f = act r (act s f)
    simp only [act, map_mul]
    rw [← aeval_algHom_apply]
    simp only [map_mul, aeval_C, algebraMap_eq, aeval_X]
    congr 2
    ring
  smul_zero r := by change act r 0 = 0; simp [act]
  smul_add r f g := by change act r (f + g) = act r f + act r g; simp [act, mul_add]
  smul_one r := by change act r 1 = 1; simp [act]
  smul_mul r f g := by change act r (f * g) = act r f * act r g; simp [act]


variable (r : R)

-- But now we have two different `Smul`s `R → R[X] → R[X]` ...

example : r • (1 : R[X]) = C r := by
  rw [← mul_one (C r), smul_eq_C_mul]

attribute [instance 100000] MulAction.toSMul MulSemiringAction.toDistribMulAction

example : r • (1 : R[X]) = 1 := smul_one r

On the one hand, there is the natural action by scalar multiplication coming from the fact that R[X] is an R-algebra. On the other hand, we may want to have another action that (for example) acts via ring homomorphisms (as in the example). And usually, we may want to use both at the same time.

So I think that it might make sense to separate true scalar multiplication (which satisfies (r + s) • x = r • x + s • x) from other actions by monoids (like docs#MulSemiringAction). This would involve two have two different notation classes (and certainly some duplication of API), but would allow having both kinds of action at the same time (and, for example, enable one to write down that they are compatible without jumping through a lot of hoops). I also think that such a separation may help with problems like the one discussed in #mathlib4 > simp timeout at `whnf` @ 💬, where simp times out because it frantically tries to apply docs#smul_X in a situation where it talks about the wrong kind of action. In particular, this could help with type class searches when SMul is involved.

What do people think?

[Eric Wieser]

I think it's not the case that MulSemiringAction can't use the notation, but rather that your particular instance of MulSemiringAction cannot

[Eric Wieser]

MulSemiringAction works fine, I believe, for the action of a ring hom on a polynomial.

[Eric Wieser]

Section 4.5 in my thesis chapter on scalar actions has an example of why these endomorphism actions are in fact not a problem

[Michael Stoll]

But it can still interact badly behind the scenes and cause slowness...

[Michael Stoll]

... even (or in particular?) when there is no MulSemiringAction actually available.

[Eric Wieser]

I don't think removing the instances or simp lemmas is the answer to the slowness

[Eric Wieser]

Or at least, I'd strongly prefer that we keep that solution as a last resort

[Michael Stoll]

I'm not suggesting to remove instances or simp attributes. Rather, the suggestion is to split the SMuls into actual scalar multiplications and other actions by monoids. This would separate the relevant instances (so that they don't interfere with each other), but not remove them. And having different notations would prevent simp from trying to use docs#smul_X when we are dealing with scalar multiplication, because the terms wouldn't match.