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.

• Adds a subtraction operator for modules
• Adds a notion of "polymorphic" module morphisms, which can change the underlying ring
• 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.

[jamesmckinna]

Do the parentheses help here? I'm not convinced...

[Taneb]

It's been a while, but I think without them Agda doesn't know if I mean that or a use of the _-ᴹ_ operator

[jamesmckinna]

Ah... I see, but still worth thinking about the earlier comment about having a small PR adding that subtraction operator in its own right?

[jamesmckinna]

So I agree with you that it's annoying to have to be explicit with these arguments... I suppose that's one way of nudging the typechecker to know which scalars are involved at a given call-/use- site in this new setup, but perhaps simply supplying the R/S arguments would be the other way to do it?

[jamesmckinna]

As I've indicated before, i think this design is trying to do too many things at once which could be usefully factored into smaller pieces, such as #2913 ?

[Taneb]

Yes, I've come to agree with you on this.

[jamesmckinna]

OK, let's see what comes out in the wash!

[Taneb]

Closing in favour of the approach described in #2913