From f7f4f434aab14d6deccaf4f2740981813d6a671a Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 30 Dec 2024 15:30:21 -0500
Subject: [PATCH] define left module composition and graded module composition

---
 src/ThesisWork/Ext.agda    | 23 ++++++++++++++++++-----
 src/ThesisWork/Graded.agda | 10 ++++++----
 2 files changed, 24 insertions(+), 9 deletions(-)

diff --git a/src/ThesisWork/Ext.agda b/src/ThesisWork/Ext.agda
index 8be464e..7669f40 100644
--- a/src/ThesisWork/Ext.agda
+++ b/src/ThesisWork/Ext.agda
@@ -20,10 +20,10 @@ module _ {R : Ring ℓ} where
     → (g : LeftModuleHom N P)
     → LeftModuleHom M P
   compLeftModule {M = M} {N} {P} f g =
-    fg , record { pres0 = pres0 ; pres+ = pres+ ; pres- = {!   !} ; pres⋆ = {!   !} } where
-      open LeftModuleStr (M .snd) using () renaming (0m to 0M; _+_ to _+M_; -_ to -M_)
-      open LeftModuleStr (N .snd) using () renaming (0m to 0N; _+_ to _+N_; -_ to -N_)
-      open LeftModuleStr (P .snd) using () renaming (0m to 0P; _+_ to _+P_; -_ to -P_)
+    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
 
@@ -39,4 +39,17 @@ module _ {R : Ring ℓ} where
         p
 
       pres- : (x : M .fst) → fg (-M x) ≡ -P (fg x)
-      pres- x = {!   !}
\ No newline at end of file
+      -- 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
diff --git a/src/ThesisWork/Graded.agda b/src/ThesisWork/Graded.agda
index c6c4121..5a9c7a0 100644
--- a/src/ThesisWork/Graded.agda
+++ b/src/ThesisWork/Graded.agda
@@ -12,6 +12,8 @@ open import Cubical.Algebra.Group.Morphisms
 open import Cubical.Algebra.Group.MorphismProperties
 open import Cubical.Foundations.Structure
 
+open import ThesisWork.Ext
+
 private
   variable
     ℓ ℓ' ℓ'' : Level
@@ -89,7 +91,7 @@ gradedHomComp {G = G} {M₁} {M₂} {M₃} (mkGradedHom feqv fp ffn) (mkGradedHo
       p
 
     fgFn : {x y : ⟨ G ⟩} → fg x ≡ y → M₁ x -[lm]→ M₃ y
-    fgFn {x} {y} p = {!   !}
-      -- p : f(g(x)) ≡ y
-      where
-        open import Cubical.Foundations.Function
\ No newline at end of file
+    fgFn {x} {y} p = compLeftModule (ffn refl) (gfn p)
+      -- p : g(f(x)) ≡ y
+      -- break into f(x) ≡ z and g(z) ≡ y for some z
+      -- just pick z = f(x) and the second can use p
\ No newline at end of file