Should Modules have raw bundles?

[Taneb]

Currently, for each bundle defined in Algebra.Bundles, there is a corresponding raw bundle, consisting of the operations but without the laws. The same is not true for Algebra.Module.Bundles. Should they be added?

[Taneb]

Further question: should there be a distinct RawSemimodule/RawModule? This works out the same as RawBisemimodule/RawBimodule with its ring argument repeated

[MatthewDaggitt]

So in general, if two structures have the same signature but different laws then we only have a single raw bundle for them.

[Taneb]

In this case we should probably remove SemimoduleMorphisms and ModuleMorphisms from Algebra.Module.Morphism.Structures. They don't add any further laws, just wrapping over the smaller BisemimoduleMorphisms and BimoduleMorphisms with different parameters. I feel bad at not having these, though.

[jamesmckinna]

I, too would feel bad, especially for the interaction with #1898 ... and the fact that BimoduleMorphisms have two fields for the homomorphism property wrt scalar multiplication. I really think that ModuleMorphisms should just have the one... and of course give rise in the usual way by duplication to the associated BimoduleMorphisms etc structure...

... but perhaps I am missing the force both of @MatthewDaggitt 's comment, and yours. But in practical terms, if I were working with modules, I shouldn't want to be dropping down into substructures for the sake of stdlib style conventions. Not being able to rename record fields is a pain, so commitments Commitments to any distinguished choice of those taking priority over others... seems like something requiring further discussion?

[jamesmckinna]

Any progress on this @Taneb ?

[Taneb]

I've just independently re-motivated myself for this. Going to give it another push, hopefully won't take long.