update

src/ThesisWork/ExactCouple.agda

@@ -0,0 +1,32 @@
+{-# OPTIONS --cubical #-}
+
+-- Extra stuff not in the cubical standard library
+
+module ThesisWork.ExactCouple where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Algebra.Ring
+open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.DirProd
+open import Cubical.Algebra.Group.Instances.Int
+
+open import ThesisWork.Graded
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+module _ {R : Ring ℓ} where
+  ℤ×ℤGroup = DirProd ℤGroup ℤGroup
+  ℤ×ℤ = ⟨ ℤ×ℤGroup ⟩
+
+  record ExactCouple : Type (ℓ-suc ℓ) where
+    field
+      D E : GradedModule R ℤ×ℤ
+      i : GradedHom R ℤ×ℤGroup D D
+      j : GradedHom R ℤ×ℤGroup D E
+      k : GradedHom R ℤ×ℤGroup E D
+
+deriveExactCouple : {R : Ring ℓ} → ExactCouple {R = R} → ExactCouple {R = R}
+deriveExactCouple = {!   !}

src/ThesisWork/Ext.agda

@@ -15,11 +15,14 @@ private
     ℓ ℓ' ℓ'' : Level
 
 module _ {R : Ring ℓ} where
-  compLeftModule : {M N P : LeftModule R ℓ'}
+  idLeftModuleHom : (M : LeftModule R ℓ') → LeftModuleHom M M
+  idLeftModuleHom M = (idfun ⟨ M ⟩) , record { pres0 = refl ; pres+ = λ x y → refl ; pres- = λ x → refl ; pres⋆ = λ r y → refl } 
+
+  compLeftModuleHom : {M N P : LeftModule R ℓ'}
     → (f : LeftModuleHom M N)
     → (g : LeftModuleHom N P)
     → LeftModuleHom M P
-  compLeftModule {M = M} {N} {P} f g =
+  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_)

src/ThesisWork/Graded.agda

@@ -18,6 +18,7 @@ private
   variable
     ℓ ℓ' ℓ'' : Level
 
+-- Using FVD's definition of graded here
 graded : Type ℓ → Type ℓ' → Type (ℓ-max ℓ ℓ')
 graded str I = I → str
 
@@ -35,6 +36,13 @@ module _ (R : Ring ℓ) (G : Group ℓ') (M₁ M₂ : GradedModule R ⟨ G ⟩)
 
   -- Graded abelian group homomorphism (definition 5.1.1 in FVD thesis)
   -- https://git.mzhang.io/michael/Spectral/src/commit/ea402f56eaf63c8668313fb4c6a382d95a45f5ea/algebra/graded.hlean#L45-L48
+  --
+  -- Wikipedia definition: A morphism (f : N → M) of graded modules,
+  -- called a graded morphism or graded homomorphism,
+  -- is a homomorphism of the underlying modules that respects grading;
+  -- i.e. f(Nᵢ) ⊆ Mᵢ.
+  --
+  -- Question: why did FVD use Equivalences here? Could I just use GroupHom?
   record GradedHom : Type (ℓ-max ℓ (ℓ-suc ℓ')) where
     constructor mkGradedHom
     field
@@ -46,10 +54,14 @@ module _ (R : Ring ℓ) (G : Group ℓ') (M₁ M₂ : GradedModule R ⟨ G ⟩)
         let e = groupEquivFun equiv in -- the function of the equivalence
         {x y : ⟨ G ⟩} → (p : e x ≡ y) → (M₁ x) -[lm]→ (M₂ y)
 
+idGradedModuleHom : {R : Ring ℓ} {G : Group ℓ'} (M : GradedModule R ⟨ G ⟩) → GradedHom R G M M
+idGradedModuleHom {G = G} M = mkGradedHom idGroupEquiv (λ g → sym (·IdR g)) (λ {x = x} p → J (λ y p → M x -[lm]→ M y) (idLeftModuleHom (M x)) p) where
+  open GroupStr (G .snd)
+
 -- Composition of graded homomorphisms
-gradedHomComp : {R : Ring ℓ} {G : Group ℓ'} {M₁ M₂ M₃ : GradedModule R ⟨ G ⟩}
+compGradedModuleHom : {R : Ring ℓ} {G : Group ℓ'} {M₁ M₂ M₃ : GradedModule R ⟨ G ⟩}
   → (f : GradedHom R G M₁ M₂) → (g : GradedHom R G M₂ M₃) → GradedHom R G M₁ M₃
-gradedHomComp {G = G} {M₁} {M₂} {M₃} (mkGradedHom feqv fp ffn) (mkGradedHom geqv gp gfn) =
+compGradedModuleHom {G = G} {M₁} {M₂} {M₃} (mkGradedHom feqv fp ffn) (mkGradedHom geqv gp gfn) =
   mkGradedHom (compGroupEquiv feqv geqv) fgp fgFn where
     -- Composition of the equivalence
     fgEqv : ⟨ G ⟩ ≃ ⟨ G ⟩
@@ -61,26 +73,6 @@ gradedHomComp {G = G} {M₁} {M₂} {M₃} (mkGradedHom feqv fp ffn) (mkGradedHo
     f = feqv .fst .fst
     g = geqv .fst .fst
     fg = fgEqv .fst
-
-    -- -- Reminder: these are definitionally equal
-    -- _ : fg ≡ λ x → g (f x)
-    -- _ = refl
-
-    -- fgEqvIsGroupEquiv : IsGroupEquiv (G .snd) fgEqv (G .snd)
-    -- -- f(g(x · y)) ≡ f(g(x)) · f(g(y))
-    -- -- f(g(x) · g(y)) ≡
-    -- -- f(g(x)) · f(g(y)) ≡
-    -- fgEqvIsGroupEquiv .pres· x y =
-    --   let p = refl {x = g (f (x · y))} in           -- g(f(x·y)) ≡ g(f(x·y))
-    --   let p = p ∙ cong g (feqv .snd .pres· x y) in  -- g(f(x·y)) ≡ g(f(x)·f(y))
-    --   let p = p ∙ geqv .snd .pres· (f x) (f y) in   -- g(f(x·y)) ≡ g(f(x))·g(f(y))
-    --   p
-    -- fgEqvIsGroupEquiv .pres1 = cong g (feqv .snd .pres1) ∙ geqv .snd .pres1
-    -- fgEqvIsGroupEquiv .presinv x =
-    --   let p = refl {x = g (f (inv x))} in           -- g(f(inv x)) ≡ g(f(inv x))
-    --   let p = p ∙ cong g (feqv .snd .presinv x) in  -- g(f(inv x)) ≡ g(inv(f x))
-    --   let p = p ∙ geqv .snd .presinv (f x) in       -- g(f(inv x)) ≡ inv(g(f x))
-    --   p
     
     fgp : (x : ⟨ G ⟩) → fg x ≡ x · fg 1g
     fgp x =
@@ -91,7 +83,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 = compLeftModule (ffn refl) (gfn p)
+    fgFn {x} {y} p = compLeftModuleHom (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

src/ThesisWork/SpectralSequence.agda

@@ -38,6 +38,7 @@ module _ (R : Ring ℓ) where
 
       -- differentials, are graded morphisms dᵣ : Eᵣ → Eᵣ such that dᵣ ◦ dᵣ = 0
       d : (s : ℕ) → E s -[gm]→ E s
-      dᵣ∘dᵣ≡0 :
-        let _∘_ = λ (x y : {!   !}) → {!   !} in
-        (s : ℕ) → ({!   !} ∘ {!   !}) ≡ {!   !}
+      dᵣ∘dᵣ≡0 : (s : ℕ) → compGradedModuleHom (d s) (d s) ≡ idGradedModuleHom (E s)
+
+      -- Isomorphisms
+      -- the cohomology of the cochain complex determined by dᵣ.