Renaming `Basis.smul`

Stream: mathlib4

[Eric Wieser]

In #14945, I define a smul action by a group on a basis characterized by (g • b) i = g • b i, and want to write lemmas about it like Basis.smul_apply.

Unfortunately, docs#Basis.smul_apply already exists, and is about docs#Basis.smul (b1 : Basis ι R S) (b2 : Basis ι' S A) : Basis (ι × ι') R A) characterized by (b1.smul b2) i = b1 i • b2 i.
I'd like to rename this definition to make room for my one.

Some name suggestions I have are:

1. Basis.smul', which matches docs#Pi.smul' in terms of the jointly-elementwise action
2. Basis.smulTower, since this is a module over a tower of algebras
3. Basis.comp / Basis.trans, as suggested by @Yaël Dillies

[Edward van de Meent]

is the thing you're describing Pi.MulAction?

[Edward van de Meent]

docs#Pi.smul_apply ?

[Edward van de Meent]

ah wait, this doesn't give the action on the type you want, only on coersions of basis elements

[Eric Wieser]

docs#Pi.smul_apply is analogous to the lemma / instance I want to add, while docs#Pi.smul_apply' is analogous to the existing docs#Basis.smul_apply

[Eric Wieser]

/poll What name should the instance satisfying (b1 • b2) i = b1 i • b2 i have

• Basis.smul (the status quo)
• Basis.smul'
• Basis.smulTower
• Basis.comp
• Basis.trans

[Edward van de Meent]

i think that calling this smul is very bad at describing that this isn't some kind of elementwise manipulation (which i expected at first), but rather a composition.

[Edward van de Meent]

and i'd like to point out that Basis.smul currently satisfies (b1 • b2) i = b1 i.1 • b2 i.2, rather

[Edward van de Meent]

given the choice between comp and trans, i'd say trans is preferable, as Basis represents an equivalence, and the order of arguments/types also matches. (typically trans a b = comp b a holds)

[Eric Wieser]

Edward van de Meent said:

and i'd like to point out that Basis.smul currently satisfies (b1 • b2) i = b1 i.1 • b2 i.2, rather

I don't know how I managed to repeatedly misread this, thanks!

[Edward van de Meent]

i know, it's subtle! hence why simply smul or smul' isn't descriptive enough, imo

[Eric Wieser]

@Riccardo Brasca, since you reviewed the PR that spawned this, perhaps you could tie-break the naming vote?

[Eric Wieser]

(or perhaps @Johan Commelin, who might also have opinions here)

[Riccardo Brasca]

I have a little preference for smulTower. Voted.

[Johan Commelin]

I don't have an opinion this time :smiley: But Basis.smulTower sounds fine to me.

[Eric Wieser]

#15036