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.

[jamesmckinna]

I guess I'll move further comments to the new issues and the associated PRs from now on.

[jamesmckinna]

Actually, there is (for me, at least) one 'leftover' question arising from this issue, but perhaps it deserves to be(come) its own issue and subsequent PR... but as with much in the Algebra.* hierarchy, it raises various questions (for me, at least) about where such constructions should live, and at what generality they should be stated, viz.:

where should we put

• the construction R ᵒᵖ of the opposite ring of a Ring R (Semiring? Group? Monoid? Magma?); ANSWER: Algebra.Construct.Flip.Op cf. PR #1900
• the 'lemma' (trivial! how trivial?) that every left R-module gives rise to a right Rᵒᵖ-module, vice versa, and conversely (how many of these phrasings are there? what's the most efficient/minimal set of such?);
• the isomorphism between R and Rᵒᵖ in the case where R is commutative (NB. they're not definitionally equal, unfortunately, because the proof of comm for one is sym of that of the other... sigh)

This last point is what is making me hesitate about unqualified assent to this issue/PR #1898 ... something nagging about isomorphism vs. on-the-nose definitional equality. But maybe the proposal is sufficiently 'symmetric' for that not to matter?

[JacquesCarette]

• Is it a lemma or a construction that every left R-module gives rise to right Rᵒᵖ-module? That will change where it ought to go.
• the isomorphism proof is a property. Algebra.Ring.Property ?

In agda-categories, we actually added extra fields here and there so that the 'op' operation would make things work on-the-nose (such as sym-assoc for Category itself). And provided helper constructors that hide that. nt-helper (for natural transformations) is used internally a lot.

[jamesmckinna]

Regarding

Is it a lemma or a construction that every left R-module gives rise to right Rᵒᵖ-module? That will change where it ought to go.

I think it is a construction, because the 'gives rise to' is specified in a particular (constructive!) way.

[jamesmckinna]

Regarding

the isomorphism proof is a property. Algebra.Ring.Property ?

I'd be happy with both the assertion, and the location. But I can't/couldn't help worrying about needing to capture the iso for all the (suitable) substructures of Ring, before finally realising the last one as the lemma/property that I wanted. So Algebra.Ring doesn't seem... quite right?

[jamesmckinna]

Apologies: It occurred to me that these discussions have again strayed from the main issue, and perhaps should be opened as a separate issue linking from PR #1900 ...?

[JacquesCarette]

You're right that this has drifted, but since I think the side discussion is also concluding, it doesn't seem worth opening a new one, just to have it end quickly. So: Since it's a construction, it shouldn't go in Algebra.Ring.Property. The construction might well be long in the same place where Module itself is defined. Or in some Algebra.Construction module (probably better that).

If the iso is about structure X, and then it's re-used for Ring, maybe Algebra.X.Property ? There really will be properties specific to each rung of the algebra ladder.

[jamesmckinna]

Hmm. OK. But I think the constructions/iso can now wait until the PR is settled. But I have one more thing for my wishlist (or a subsequent PR after #1898... ;-)) namely that every (commutative)(semi)ring should also give rise to the appropriate module structure over itself: candidate module Algebra.Module.Construct.Self?

[Taneb]

Hmm. OK. But I think the constructions/iso can now wait until the PR is settled. But I have one more thing for my wishlist (or a subsequent PR after #1898... ;-)) namely that every (commutative)(semi)ring should also give rise to the appropriate module structure over itself: candidate module Algebra.Module.Construct.Self?

@jamesmckinna if you mean what I think you mean, then that exists! Under the somewhat non-obvious name of Algebra.Module.Construct.TensorUnit

[jamesmckinna]

Yes, of course! Thanks very much! That will greatly simplify my work on Algebra.Module.Construct.Nagata

[MatthewDaggitt]

Yup I agree with @JacquesCarette on the placement issue. Constructions should go in the Algebra.Construct folder, while non-constructions or concrete instantiations of those constructions should go in Algebra.X.Properties.

[jamesmckinna]

So... having just completed (to my satisfaction at least) pr #1910 (cleaning up the mess of #1900 ) it occurs to me that... an R-module for commutative R should (?) be an R-Rop bimodule? I was surprised, but perhaps shouldn't be, that Rop for commutative R is not a no-op...

... and inserting the op above would ensure that your condition would hold definitionally ?

or have I (once again) overlooked something obvious?

[Taneb]

@jamesmckinna I believe the counterexample I brought up back in https://github.com/agda/agda-stdlib/issues/1888#issuecomment-1362920174 would still apply here. The ring of Gaussian integers is commutative. We can define a ℤ[i]-ℤ[i]op bimodule where the left and right multiplications are conjugate to each other rather than equal.

[jamesmckinna]

@Taneb yes, of course... what I had in mind was that by taking R-Rop as the R-S bimodule structure, your axiom about left- and right- multiplication being identified would be realisable by ... refl (and that that seems to be the only 'reasonable choice? I think I'd hate to have to make it Setoid equality of Op₂ A functions, by way of contrast...?)

[MatthewDaggitt]

@Taneb was this entirely fixed by https://github.com/agda/agda-stdlib/pull/1898?

[Taneb]

Yes, it is fixed