define left module composition and graded module composition

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 = {!   !}
+      -- 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

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
+    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