Consequences of module monomorphisms

[Taneb]

Progess:

• Left semimodules
• Left modules
• Right semimodules
• Right modules
• Bisemimodules
• Bimodules
• Semimodules
• Modules

Creating this PR now to get feedback as soon as possible. I'm intending to add to it as I have the energy.

[jamesmckinna]

Can we have a global comment about the purpose of the PR?

IIUC, a ...ModuleMonomorphism allows you to induce a particular Is...Module structure on the source Raw...Module bundle by pulling back along the monomorphism... ie lifting On._on_ from Relation.Binary/Function to a particular algebraic structure? It feels as though we ought (sic) to be able to abstract over this in some more generic way? Or then again, from experience with stdlib, maybe not... yet. But I can't help thinking that all the Algebra.*.Monomorphism modules might better be refactored... somehow? Apologies if this remark is also out-of-scope for the PR at hand, and should be a style-guide/library-design or README.Design.Hierarchy issue instead?

[Taneb]

@jamesmckinna I'm not sure what you're asking for there. I don't think Relation.Binary.Construct.On significantly helps us here and I can't think of a way of doing this more generically without a colossal amount of risky work. But this is an obvious missing piece, and useful for my next goal of defining Ideals.

[jamesmckinna]

OK @Taneb I'll try to rephrase my question, but happy to do so later downstream.
But in any case, a link back to your #2076 would have been helpful (to me, at least) for context...

[jamesmckinna]

I think I'd been trying to understand what you were doing in (something like) the following terms (a lifting property from AbGrp to R-Module arising from a monadic situation):

• if you have an AbelianGroupMonomorphism between the underlying AbelianGroups of two modules, and it's a module homomorphism, then you actually have a module monomorphism;
• hence (cf. Algebra.Structures.Biased etc.), it suffices to supply 'simpler' data in order to actually have 'richer' structure, moreover automatically... ie to construct an ideal of a ring R it suffices to supply 'an Abelian subgroup which is closed under multiplication'...

But it seems as though what you have is doing something else here?

[jamesmckinna]

As for doing things generically, yes, your point is well-made. But I think the 'lifting' idea above is something to look out for generally when thinking about 'concrete categories' such as Group over Setoid and R-Mod over AbGrp...? (perhaps the agda-categories gang can give chapter and verse here?)

[JacquesCarette]

I think @jamesmckinna is simply asking: can you explain in plain English what you are trying to achieve here? It's not clear just from the code itself.

[Taneb]

What I'm trying to achieve here: I want a quick and easy way to prove that I have a module given that I have a raw module and a monomorphism to some other module.

[jamesmckinna]

Re: the discussion above about renaming directives vs. private module defs, one reason for the gymnastics in the first place might be our failure to adopt the related idioms discussed in the recent agda/agda#7118 and related material (eg. Conal's message on the Zulip...)? Still not sure if I quite understand what is at stake there, but anything to try to reduce the amount of boilerplate involved with the Algebra.* hierarchy (as I am discovering on #2296 ...)

[jamesmckinna]

Looking at the parametrisation of the various constructions, I can't help but see this as further argument in favour of #2252 , but in any case without having to address that issue head-on, you might still consider making all of these definitions inside anonymous modules which would allow you to avoid the [DRY] anti-pattern of opening a locally-defined module using let in the type of an definition, and then having to repeat yourself with a corresponding where clause in the body ...?

But taking #2252 more seriously, your operations coul all be parametrised on RawX bundles, rather than their flattened versions, and then open them locally in the types/definitions as above in order to obtain the exact symbols you require for the IsX assumptions...?

If I had more time today, I'd re-draft a specimen instance for comparison... but that will have to wait for now.

UPDATED: my proposal founders on the coupling of RawX bundles with their Carrier sets, when your constructions already take those sets as parameters to the module... grrr. Comments about DRY still apply, but I can't quite do what I would really like to do without separately introducing 'RawStructures... ie the Signatures parametrised on a Set proposed in #2252 .. sigh.

[Taneb]

@jamesmckinna I've made things a bit simpler with modules. Thanks for the suggestion! I don't know how much #2252 will help, though

[jamesmckinna]

This a PROVISIONAL approve review.
Everything looks good, but there seems to be an excess of opening of structures which end up not being used... so will nit-pick in what follows...

[jamesmckinna]

Comments are largely nitpicks/questions of style.

That said: needs CHANGELOG!

[jamesmckinna]

I find this a bit hard to read/understand; might it be better to 'localise' the names here to N, as eg,

module _ (+ᴺ-isMagma : IsMagma N._≈ᴹ_ N._+ᴹ_) where

  open IsMagma +ᴺ-isMagma
    using (setoid)
    renaming (∙-cong to +ᴺ-cong)

[jamesmckinna]

And perhaps even on L20 above write:

open module N = ... renaming (_≈ᴹ_ to _≈ᴺ_; _+ᴹ_ to _+ᴺ_)

Ordinarily, I'd be again such renaming, but I find the notation N._+ᴹ_ horrible to read, even if unambiguous...

[jamesmckinna]

Similarly?

module R = Ring (record { isRing = R-isRing })

[jamesmckinna]

Either way, whitespace missing in record { isRing = R-isRing }!

[jamesmckinna]

As above, mutatis mutandis, for LeftSemimoduleMonomorphism...? Etc.

[jamesmckinna]

This time, +ᴹ-cong is nowhere used... so using (setoid) would suffice?

[jamesmckinna]

Sorry that this has taken so long to review!

UPDATED thanks for the thoughtful response to all my nitpicks. I'm happy to proceed with things as you have them, modulo the last few outstanding comments about consistency of locally-introduced module names etc. Some of the code is still pretty hard to read!

[jamesmckinna]

Elsewhere you use M and N where here you have M₁ and M₂?
Does it make sense to (try to) standardise on one or the other throughout this PR?

[gallais]

Ready to go!