[ add ] left- and right- actions induced by a Magma homomorphism

[jamesmckinna]

A simple piece of 'infrastructure' for Algebra.

NB. used extensively (implicitly) in #2854 etc. cf. #2892 and #2350 .

Issues:

• need to sort out the re-exporting strategy, plus suitable renaming (NOW: DONE?)

[Taneb]

I think this is a good addition, but if these are getting reexported by the various variations of ring morphisms, they should be renamed ⟦_⟧+_ and _+⟦_⟧ (and we should also have ⟦_⟧*_ and _*⟦_⟧, and probably something for module and lattice homomorphisms)

[jamesmckinna]

I think this is a good addition, but if these are getting reexported by the various variations of ring morphisms, they should be renamed ⟦_⟧+_ and _+⟦_⟧ (and we should also have ⟦_⟧*_ and _*⟦_⟧, and probably something for module and lattice homomorphisms)

Latest commit adds some of these export renamings. More to follow later, or downstream... most of the multiplicative substructure isn't opened in Structures, and I'm not sure what is gained by trying to chase down client openings... but agree that Lattice and Module might/should benefit from these things as well.

UPDATED: added renamed exports for Lattice and Module morphisms; the multiplicative structure of ring-like morphisms doesn't actually seem ever to be opened in stdlib, so no renaming export changes needed, it would seem?

[Taneb]

Even if they're not currently opened, it might be worth opening them specifcally to export ⟦_⟧*_ and _*⟦_⟧?

[jamesmckinna]

Even if they're not currently opened, it might be worth opening them specifcally to export ⟦_⟧*_ and _*⟦_⟧?

Good suggestion! Incoming commits...

[JacquesCarette]

I'm not keen on this design.

[JacquesCarette]

Fairbairn threshold? Do we really gain anything by adding these synonyms? The code already says we lose a bit (via the need to add hiding).

Personally I think that IsMagmaHomomorphism should be more minimalistic, and we should also have accompanying "extra kit" modules that we can use when needed. I've partially refactored agda-categories in that direction. And, in that case, seriously shrank the size of .agdai files and load times. I don't expect such an effect for Magma-related stuff, but this more "kitchen-sink" design approach is exactly what made working with Monoidal Categories so heavy.

[jamesmckinna]

Thanks @JacquesCarette for yet further ammunition in the perennial 'wide vs. narrow' API debate... but echoing comments of yours elsewhere, I don't regard the inefficiencies in Agda's allocation/usage of records in terms of memory (and hence time) as an intrinsic quality of any design for stdlib, rather that I guess I'm more willing (certainly than you) to trade off DRY (and 'standardised' vocabulary to go along with it) against YAGNI (or if you are going to need it, install an extender/connector module to afford such functionality). Of course, at least if understand your nudge correctly, you envisage these things coexisting, albeit at the cost of (proliferation and import) of such extender modules...

I (perhaps) agree that stdlib somehow should aim to accommodate both ends of this spectrum, but as the Algebra.* hierarchy develops, it does seem clear that a number of infrastructural definitional extensions of the the 'basic' signature(s) seem to emerge as pervasive once we move to developing (short) exact sequences and their associated sub-/quotient structures cf. the PRs identified in the preamble.

Against that, I do (perhaps) accept the appeal to Fairbairn, although again, once we get to action and wreath products, I'm not so sure... these 'crossed'/'semidirect' reindexed actions seem to arise everywhere? And the programme of constructive explicitation of mathematics which our proof assistants instrument seems concomitantly to expose the need to identify the infrastructure otherwise implicit in many branches of axiomatic algebra? (Maybe not; it's a discussion point, just as this PR was in part a prompt to such discussion...)

[jamesmckinna]

After sleeping on this, I'll convert to DRAFT in the interim, against refactoring along the lines suggested by @JacquesCarette ...