[ 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...