Module morphisms polymorphic in the underlying ring structure

[Taneb]

This was a side-experiment in #2729 that I separated out so it could get feedback without hindering that PR. It is neither blocking nor blocked by that PR.

• [x] Adds a subtraction operator for modules
• [x] Adds a notion of "polymorphic" module morphisms, which can change the underlying ring
• [x] Redefines "monomorphic" module morphisms in terms of these
• [ ] Properties of polymorphic monomorphisms

I'm frustrated that defining monomorphic module morphisms in terms of polymorphic ones messes with the (Agda) module parameters needed downstream. I'm not sure why they need to be made explicit

[jamesmckinna]

Maybe I'm missing something, but I'm not clear about the (eventual) pragmatics/uses of this design, compared with factorising any X-module morphism between M and N over two distinct X-rings of coefficients R and S, related by a X-ring homomorphism h

• a morphism relative to S between h*N and N
• a morphism between M and h*N relative to R
• .. for a suitable definition of ... ah, now I perhaps see.

But still, documenting the rationale for the design as part of the PR documentation, if not as commentary in the files themselves, would be useful, I think. As to unsolved metas/need for explicit arguments, that seems to be a recurring problem with Agda's (weakened) mechanisms for inferring such things in the setting of the more complicate flags/modality/erasure/polarity analyses now being instrumented?

UPDATED:

• suggest that the addition of a binary subtraction operator (inherited from the underlying +-abelianGroup of a module?) be lifted out as a separate PR, if it's useful...
• revisiting my earlier comment, maybe it is simpler to reconsider this PR in terms of a Construct on XModules of 'change-of-base along a homomorphism of coefficients' h* M, and then your new composite 'polymorphic' notion of homomorphism as being given definitionally as a 'monomorphic' homomorphism between M and h * N? And certainly, that wouldn't require the new explicit parametrisation?

[JacquesCarette]

I agree that more documentation would have been helpful.

From what I can see from the code:

1. I really want this capability,
2. but not as a modification of the current code,
3. rather as a different kind of module morphism.

[jamesmckinna]

@JacquesCarette does the change-of-base construction give you what you want, as suggested above?

[JacquesCarette]

does the change-of-base construction give you what you want?

Quite likely. But the devil's in the details for such things, thus my hedging.