From c9572e9f31e0bdaa99e17d90646907dacbcb1690 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 30 Dec 2024 15:52:10 -0500
Subject: [PATCH 1/3] implement composition of left module homomorphisms

---
 Cubical/Algebra/Module/Properties.agda | 50 ++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)

diff --git a/Cubical/Algebra/Module/Properties.agda b/Cubical/Algebra/Module/Properties.agda
index ded3e46c7e..74db6ecb4c 100644
--- a/Cubical/Algebra/Module/Properties.agda
+++ b/Cubical/Algebra/Module/Properties.agda
@@ -3,6 +3,7 @@ module Cubical.Algebra.Module.Properties where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Function using (idfun; _∘_)
 
 open import Cubical.Algebra.Module.Base
 open import Cubical.Algebra.Ring
@@ -43,3 +44,52 @@ module ModuleTheory (R : Ring ℓ') (M : LeftModule R ℓ) where
        (R.1r R.+ (R.- R.1r))  ⋆ x  ≡⟨ congL _⋆_ (R.+InvR R.1r) ⟩
        R.0r                   ⋆ x  ≡⟨ ⋆AnnihilL x ⟩
        0m ∎)
+
+  idLeftModuleHom : (M : LeftModule R ℓ') → LeftModuleHom M M
+  idLeftModuleHom M = (idfun ⟨ M ⟩) , isLeftModuleHom where
+    open IsLeftModuleHom
+    isLeftModuleHom : IsLeftModuleHom (M .snd) (idfun ⟨ M ⟩) (M .snd)
+    isLeftModuleHom .pres0 = refl
+    isLeftModuleHom .pres+ x y = refl
+    isLeftModuleHom .pres- x = refl
+    isLeftModuleHom .pres⋆ r y = refl
+
+  -- Composition of left module homomorphisms
+  compLeftModuleHom : {M N P : LeftModule R ℓ'}
+    → (f : LeftModuleHom M N)
+    → (g : LeftModuleHom N P)
+    → LeftModuleHom M P
+  compLeftModuleHom {M = M} {N} {P} f g =
+    fg , record { pres0 = pres0 ; pres+ = pres+ ; pres- = pres- ; pres⋆ = pres⋆ } where
+      open LeftModuleStr (M .snd) using () renaming (0m to 0M; _+_ to _+M_; -_ to -M_; _⋆_ to _⋆M_)
+      open LeftModuleStr (N .snd) using () renaming (0m to 0N; _+_ to _+N_; -_ to -N_; _⋆_ to _⋆N_)
+      open LeftModuleStr (P .snd) using () renaming (0m to 0P; _+_ to _+P_; -_ to -P_; _⋆_ to _⋆P_)
+
+      fg = g .fst ∘ f .fst
+
+      pres0 : fg 0M ≡ 0P
+      pres0 = cong (g .fst) (f .snd .IsLeftModuleHom.pres0) ∙ g .snd .IsLeftModuleHom.pres0
+      
+      pres+ : (x y : M .fst) → fg (x +M y) ≡ fg x +P fg y
+      -- g(f(x+y)) ≡ g(f(x)+f(y)) ≡ g(f(x))+g(f(y))
+      pres+ x y =
+        let p = refl {x = g .fst (f .fst (x +M y))} in
+        let p = p ∙ cong (g .fst) (f .snd .IsLeftModuleHom.pres+ x y) in
+        let p = p ∙ g .snd .IsLeftModuleHom.pres+ (f .fst x) (f .fst y) in
+        p
+
+      pres- : (x : M .fst) → fg (-M x) ≡ -P (fg x)
+      -- g(f(-x)) ≡ g(-f(x)) ≡ -g(f(x))
+      pres- x =
+        let p = refl {x = g .fst (f .fst (-M x))} in
+        let p = p ∙ cong (g .fst) (f .snd .IsLeftModuleHom.pres- x) in
+        let p = p ∙ g .snd .IsLeftModuleHom.pres- (f .fst x) in
+        p
+
+      pres⋆ : (r : ⟨ R ⟩) (y : M .fst) → fg (r ⋆M y) ≡ r ⋆P fg y
+      -- g(f(r⋆y)) ≡ g(r⋆f(y)) ≡ r⋆g(f(y))
+      pres⋆ r y =
+        let p = refl {x = g .fst (f .fst (r ⋆M y))} in
+        let p = p ∙ cong (g .fst) (f .snd .IsLeftModuleHom.pres⋆ r y) in
+        let p = p ∙ g .snd .IsLeftModuleHom.pres⋆ r (f .fst y) in
+        p
\ No newline at end of file

From 5d40c0692e9704a1ef59119cfd99048f12f93cf5 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 30 Dec 2024 16:02:13 -0500
Subject: [PATCH 2/3] pull out to top level

---
 Cubical/Algebra/Module/Properties.agda | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/Cubical/Algebra/Module/Properties.agda b/Cubical/Algebra/Module/Properties.agda
index 74db6ecb4c..b7f58e2d0a 100644
--- a/Cubical/Algebra/Module/Properties.agda
+++ b/Cubical/Algebra/Module/Properties.agda
@@ -45,8 +45,9 @@ module ModuleTheory (R : Ring ℓ') (M : LeftModule R ℓ) where
        R.0r                   ⋆ x  ≡⟨ ⋆AnnihilL x ⟩
        0m ∎)
 
-  idLeftModuleHom : (M : LeftModule R ℓ') → LeftModuleHom M M
-  idLeftModuleHom M = (idfun ⟨ M ⟩) , isLeftModuleHom where
+module _ {R : Ring ℓ'} (M : LeftModule R ℓ) where
+  idLeftModuleHom : LeftModuleHom M M
+  idLeftModuleHom = (idfun ⟨ M ⟩) , isLeftModuleHom where
     open IsLeftModuleHom
     isLeftModuleHom : IsLeftModuleHom (M .snd) (idfun ⟨ M ⟩) (M .snd)
     isLeftModuleHom .pres0 = refl
@@ -54,12 +55,10 @@ module ModuleTheory (R : Ring ℓ') (M : LeftModule R ℓ) where
     isLeftModuleHom .pres- x = refl
     isLeftModuleHom .pres⋆ r y = refl
 
+module _ {R : Ring ℓ'} {M N P : LeftModule R ℓ} where
   -- Composition of left module homomorphisms
-  compLeftModuleHom : {M N P : LeftModule R ℓ'}
-    → (f : LeftModuleHom M N)
-    → (g : LeftModuleHom N P)
-    → LeftModuleHom M P
-  compLeftModuleHom {M = M} {N} {P} f g =
+  compLeftModuleHom : LeftModuleHom M N → LeftModuleHom N P → LeftModuleHom M P
+  compLeftModuleHom f g =
     fg , record { pres0 = pres0 ; pres+ = pres+ ; pres- = pres- ; pres⋆ = pres⋆ } where
       open LeftModuleStr (M .snd) using () renaming (0m to 0M; _+_ to _+M_; -_ to -M_; _⋆_ to _⋆M_)
       open LeftModuleStr (N .snd) using () renaming (0m to 0N; _+_ to _+N_; -_ to -N_; _⋆_ to _⋆N_)

From 7709591260118d24119fb08bbeca692bdca285b7 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 30 Dec 2024 16:02:41 -0500
Subject: [PATCH 3/3] fix whitespace

---
 Cubical/Algebra/Module/Properties.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cubical/Algebra/Module/Properties.agda b/Cubical/Algebra/Module/Properties.agda
index b7f58e2d0a..8b90ba0747 100644
--- a/Cubical/Algebra/Module/Properties.agda
+++ b/Cubical/Algebra/Module/Properties.agda
@@ -68,7 +68,7 @@ module _ {R : Ring ℓ'} {M N P : LeftModule R ℓ} where
 
       pres0 : fg 0M ≡ 0P
       pres0 = cong (g .fst) (f .snd .IsLeftModuleHom.pres0) ∙ g .snd .IsLeftModuleHom.pres0
-      
+
       pres+ : (x y : M .fst) → fg (x +M y) ≡ fg x +P fg y
       -- g(f(x+y)) ≡ g(f(x)+f(y)) ≡ g(f(x))+g(f(y))
       pres+ x y =
@@ -91,4 +91,4 @@ module _ {R : Ring ℓ'} {M N P : LeftModule R ℓ} where
         let p = refl {x = g .fst (f .fst (r ⋆M y))} in
         let p = p ∙ cong (g .fst) (f .snd .IsLeftModuleHom.pres⋆ r y) in
         let p = p ∙ g .snd .IsLeftModuleHom.pres⋆ r (f .fst y) in
-        p
\ No newline at end of file
+        p