Is star_module sensible for non-commutative rings?

Stream: maths

[Eric Wieser]

docs#star_module has as its defining property that:

star_smul : ∀ (r : R) (a : A), star (r • a) = star r • star a

Is this the right choice of definition? Would we expectstar_module ℍ[R] (ι → ℍ[R])to be true? (it's not with this definition)

If so, then a better definition might be

star_smul : ∀ (r : R) (a : A), star (r • a) = op (star r) • star a

[Reid Barton]

It does seem like the definition forces the action to be commutative, that is $rsa = sra$ for any $r$, $s \in R$, $a \in A$, even when $R$ itself is not commutative. Equivalently the action factors through the commutative ring $R/[R,R]$. This is under the other assumptions listed at docs#star_module (star is involutive and $A$ is an $R$-module, etc.)

[Reid Barton]

Eric Wieser said:

If so, then a better definition might be

star_smul : ∀ (r : R) (a : A), star (r • a) = op (star r) • star a

I'm not sure what this is supposed to mean, are you suggesting that $A$ should be a bimodule?

[Reid Barton]

I guess the intended examples of star_module in its current form are with $R$ a commutative ring but with nontrivial star structure, like $\mathbb{C}$ or $\mathbb{C}[X,Y,Z]$ or the ring of continuous complex-valued functions on some space. In that case it does seem more useful to consider modules (e.g. sections of a complex vector bundle with a real structure), not bimodules.

[Eric Wieser]

I'm not sure what this is supposed to mean, are you suggesting that A should be a bimodule?

Yes, I'm suggesting it should apply to cases when A is a left- and right- R-module. Is there a reason to avoid bi-modules beside the obvious lack of API around them?

[Eric Wieser]

For commutative rings you could have a typeclass equal_bimodule R A that says op r • a = r • a, to make all the ops go away for the cases like the ones you describe.

[Reid Barton]

If all you care about is modules over a commutative ring then it's a bit artificial to instead treat them as bimodules where the two actions agree. Otherwise, I agree with what you say.

[Eric Wieser]

Would any of symmetric_bimodule, simple_bimodule, and trivial_bimodule be a better name?

[Eric Wieser]

Eric Wieser said:

Would any of symmetric_bimodule, simple_bimodule, and trivial_bimodule be a better name?

This now exists as docs#is_central_scalar, which has about 50 instances.

[Eric Wieser]

I'm now running into some other annoyances with star_module in #13938

[Eric Wieser]

Should we put a trivial star structure on nat, int, and rat so that we can make those actions count as star modules?