Naming discrepancy: `smulLeft` vs `smulRight`

Stream: mathlib4

[David Loeffler]

Trivial issue of the day: in mathlib, bundled versions of the map fun v ↦ k • v (with fixed k, and v as the argument) are sometimes called smulLeft and sometimes smulRight!

import Mathlib

variable {K V : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] (k : K) (hk : k ≠ 0)

example : (AddMonoidHom.smulLeft k : V → V) = fun v ↦ k • v := rfl

example : (Equiv.smulRight hk : V → V) = fun v ↦ k • v := rfl

I spotted this because I wanted to make an AddEquiv version (it would have saved a line or two in #29914), which would have extended both AddMonoidHom.smulLeft and Equiv.smulRight, and I couldn't work out what to call it.

I think Equiv.smulRight is the one that's wrong here, and should become Equiv.smulLeft. Is this worth fixing, or should we leave it be (and tolerate the naming inconsistency) for the sake of not breaking existing code?

[Eric Wieser]

Is the equiv version docs#DistribMulAction.toAddAut ?

[Eric Wieser]

Equiv.smulRight is really just docs#MulAction.toPerm combined with docs#Units.mk0

[Eric Wieser]

arguably docs#AddMonoidHom.smulLeft should just be deleted, it's just an alias of docs#DistribMulAction.toAddMonoidHom

[David Loeffler]

Eric Wieser said:

Is the equiv version docs#DistribMulAction.toAddAut ?

Not quite, since K isn't a group, only a GroupWithZero (and we don't have a concept of DistribMulActionWithZero).

[David Loeffler]

Eric Wieser said:

arguably docs#AddMonoidHom.smulLeft should just be deleted, it's just an alias of docs#DistribMulAction.toAddMonoidHom

Maybe, but we also have e.g. docs#ContinuousLinearEquiv.smulLeft, docs#OrderIso.mulLeft, docs#LinearMap.mulLeft, etc.

[Eric Wieser]

DistribMulAction.toAddEquiv (Units.mk0 v hv) would presumably suffice for the GroupWithZero case

[Eric Wieser]

I guess we could add shorthands for each of these Units.mk0 versions by appending a \0 to the other name

[David Loeffler]

That is indeed is a very elegant way of implementing it. But I think you are not appreciating quite how utterly trivial my question is here: What should it be called? :slight_smile:

Should it be AddEquiv.smulLeft₀ (consistently with AddMonoidHom.smulLeft), or AddEquiv.smulRight₀ (consistently with Equiv.smulRight)?

[Eric Wieser]

I claim it should be called DistribMulAction.toAddEquiv₀

[Eric Wieser]

Either that or we should rename the entire family of DistribMulAction.toAddEquiv declarations, of which I would guess there are 10-20:

• docs#MulAction.toEndHom, docs#MulAction.toPerm, docs#MulAction.toPermHom
• docs#DistribMulAction.toAddMonoidHom, docs#DistribMulAction.toAddMonoidEnd, docs#DistribMulAction.toAddEquiv, docs#DistribMulAction.toAddAut, docs#DistribMulAction.toLinearMap, docs#DistribMulAction.toModuleEnd, docs#DistribMulAction.toLinearEquiv, docs#DistribMulAction.toModuleAut
• docs#Module.toModuleEnd
• docs#Algebra.lsmul (refers to the pattern in the docstring)

[David Loeffler]

Hmm... that's a lot of renaming to no clear benefit; I was just trying to resolve the left-right ambiguity, not anything beyond that.

How about the following proposal?

• create DistribMulAction.toAddEquiv₀, but also make AddEquiv.smulLeft₀ an alias for it
• rename the existing Equiv.smulRight to Equiv.smulLeft₀ (deprecating the old name as usual)?

[Eric Wieser]

Perhaps those should be changed to aliases too?

[David Loeffler]

Eric Wieser said:

Perhaps those should be changed to aliases too?

Which ones? Do you mean that we should haveMulAction.toPerm₀, and Equiv.smulLeft₀ should be an alias for it?