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

Author: jamesmckinna

CHANGELOG.md

@@ -151,6 +151,12 @@ Additions to existing modules
   ⊕-∧-booleanRing   : BooleanRing _ _
   ```
 
+* In `Algebra.Morphism.Structures.IsMagmaHomomorphism`:
+  ```agda
+  ⟦_⟧∙_ : A → B → B
+  _∙⟦_⟧ : B → A → B
+  ```
+
 * In `Algebra.Properties.RingWithoutOne`:
   ```agda
   [-x][-y]≈xy : ∀ x y → - x * - y ≈ x * y

src/Algebra/Morphism/Structures.agda

@@ -89,6 +89,12 @@ module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) wher
     open IsRelHomomorphism isRelHomomorphism public
       renaming (cong to ⟦⟧-cong)
 
+    ⟦_⟧∙_ : A → B → B
+    ⟦ x ⟧∙ y = ⟦ x ⟧ ◦ y
+
+    _∙⟦_⟧ : B → A → B
+    y ∙⟦ x ⟧ = y ◦ ⟦ x ⟧
+
 
   record IsMagmaMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field