Should Semimodules and Modules have a rule saying that left- and right-multiplication are the same?

[Taneb]

i.e. ∀ x m → x *ₗ m ≈ᴹ m *ᵣ x.

This can't be stated for Bisemimodule and Bimodule but for Semimodule and Module it feels a useful property to have that we can't currently prove for a general module.

[MatthewDaggitt]

I have no idea about module theory, so I'm not really equipped to answer this one.

[jamesmckinna]

I've been doing some work recently with modules, and I think this property is not in general provable. But best place to ask: mathoverflow imho

[Taneb]

I've found an example of a module (by our definition) where the two operations are different.

Take G to be the usual commutative of Gaussian integers (complex numbers of the form x + i*y for x, y integers).

Then G acts as a left module over itself with multiplication.
We can also take G to be a right module over itself with the operation \x y -> x * conjugate y.

With these two definitions, we can build a module according to stdlib's understanding of the term. See here: https://gist.github.com/Taneb/64cd57ef1896a820b27921131cfab5a6

I claim this is strongly undesirable.

[JacquesCarette]

It took me a while to reconstruct what @Taneb found objectionable, so I'll expand it out in this comment: normally a module has a single notion of multiplication, not a left one and a right one. If one builds up module by joining left/right modules, then it's possible to create a module where they are different.

The fundamental issue here is that there is no simple syntactic embedding going on here. The relation between the theories involved are an almost-trivial theorem, but not a trivial theorem (i.e. the proof is not exactly 'refl').

The simplest fix is as the title says: it should be an axiom that left- and right- multiplication amount to the same thing. They are not quite 'the same' in the strong sense of 'the same', but they are trivially equivalent...

[jamesmckinna]

But see also the discussion on MO about left/right modules, as well as this MO discussion about rings not iso to their opposites which links from the first; also this other MO discussion on left/right modules (with an extensive answer) and yet another MO discussion of left/right modules.

Notwithstanding @Taneb 's wish to avoid a "strongly undesirable" state of affairs, I wonder if the designers of Algebra.Module.Structures might need to reconsider their definitions? I confess I don't know how to reconcile the examples given above with @JacquesCarette 's assertion that the left and right- actions are "trivially equivalent".

Sorry for adding endless links to discussion of this. The definitive answer appears to be here, which clearly says that the concept of an (R,S)-module makes sense, and that
EDITED (R,R)-modules need not be R-modules even if R is commutative (previously, I just mentioned the non-commutative case).

(JC: edited comment to make it more self-contained so that people don't have to click-through to know what each links says)

[JacquesCarette]

Upshot: it seems to make sense to define (R,S)-module, which is actually what is currently implemented. It then makes sense to define R-module only for commutative rings R. (Or, at least, I think that's the conclusion to draw from all those MO posts.)

[jamesmckinna]

Jacques, thanks for the sensitive editing. But I draw/drew the opposite conclusion to you! (Especially because the noncommutative case ought not to have to take a back seat for the sake of the common case).

From my reading, the MO examples surely (?) make clear that the notion of R-S-bimodule is independently of interest... and that in the commutative case, one should prove the lemma that a left-module structure gives rise to a right module structure, and hence, if somewhat boringly, an R-R-bimodule structure.

The hard choice is how to bias the left/right choice when defining 'module'. But the articles are clear there, too, at least as I understand them: you actually have to choose, and similarly to the above, prove the lemma that a left R-module is (almost automatically) a right Rop-module.

[JacquesCarette]

Opposite? I too drew the conclusion that R-S-bimodules are of independent interest, and perhaps the most natural definition to arrive at 'structurally'. How to then also define reasonably convenient "traditional" R-modules remains open. My conclusion is that maybe it should not be defined structurally.

EDIT: meant to put 'not' in there!

[jamesmckinna]

Hmm, perhaps I see your point, but do you further intend that in the commutative R case

• the left- and right- multiplications should be made definitionally equal? and
• the notion of R-R-bimodule is retained, and remains strictly weaker?

In the first, that still feels as though the user needs to commit to making a biased choice when defining any particular instance of such structure, even if you were to have (additional) smart constructors to do the identifications for you?

EDITED: Just seen your subsequent response. Apologies if talking at cross purposes. But it seems that in the commutative case, one ends up having to make a biased choice anyway.

[jamesmckinna]

And the relevant definition in Algebra.Module.Structures does need to be changed:

  -- An R-module is an R-R-bimodule where R is commutative.
  -- This means that *ₗ and *ᵣ coincide up to mathematical equality, though it
  -- may be that they do not coincide up to definitional equality.

EDITED: but the library designers clearly had the original intention to follow @Taneb's lead...:
from Algebra.Module.Bundles

--   - Modules are bimodules with a single sort of scalars and scalar
--     multiplication must also be commutative. Left-scaling and
--     right-scaling coincide.

[Taneb]

@JacquesCarette what do you mean by "defined structurally" here?

[JacquesCarette]

@Taneb I meant that a definition that inherits from lower things, the way the 'hierarchy' in Algebra is currently done, in a straight syntactic manner. By non-structural, I was thinking of a more-or-less direct definition of R-module, from which you could reconstruct an R-R-bimodule structure via a function rather than as a projector of fields.

@jamesmckinna Yes, I think R-R-bimodule seems to be a strictly weaker notion. And yes, I mean for the left- and right- multiplications to be definitionally equal by, in fact, only storing a single multiplication in the structure itself.