wip

.vscode/settings.json

@@ -5,5 +5,4 @@
 	"gitdoc.commitMessageFormat": "'auto gitdoc commit'",
 	"agdaMode.connection.commandLineOptions": "--without-K",
 	"search.exclude": {},
-	"editor.fontFamily": "'PragmataPro Mono Liga', 'Droid Sans Mono', 'monospace', monospace"
 }

src/AOP/Focus.agda

@@ -105,9 +105,19 @@ data All> (P : A → Set) : List> A → Set where
 
 -- Every element in a list can be focused on
 focus : (xs : List> A) → All> (_∈ xs) xs
-focus list = iter-focus list list ([<] , refl) where
+focus list = iter-focus list list [<] refl where
   open import Relation.Binary.PropositionalEquality using (_≡_; subst; sym; refl)
-  open import Data.Product using (∃)
-  iter-focus : (list : List> A) (remain : List> A) (p : ∃ (λ sx → list ≡ sx <>> remain)) → All> (_∈ list) remain
-  iter-focus list [>] (sx , eq) = [>]
-  iter-focus list (x :> remain) (sx , eq) = subst (λ l → x ∈ l) (sym eq) (sx [ x ] remain) :> (iter-focus list remain ((sx :< x) , eq))
+  iter-focus : (list right : List> A) (left : List< A) (p : left <>> right ≡ list) → All> (_∈ list) right
+  iter-focus list [>] left p = [>]
+  iter-focus list (x :> right) left p =
+    let x-in-list = subst (x ∈_) p (left [ x ] right) in
+    let remain-proof = iter-focus list right (left :< x) p in
+    x-in-list :> remain-proof
+  
+  
+  -- iter-focus list list ([<] , refl) where
+  -- open import Relation.Binary.PropositionalEquality using (_≡_; subst; sym; refl)
+  -- open import Data.Product using (∃)
+  -- iter-focus : (list : List> A) (remain : List> A) (p : ∃ (λ sx → list ≡ sx <>> remain)) → All> (_∈ list) remain
+  -- iter-focus list [>] (sx , eq) = [>] 
+  -- iter-focus list (x :> remain) (sx , eq) = subst (λ l → x ∈ l) (sym eq) (sx [ x ] remain) :> (iter-focus list remain ((sx :< x) , eq))

src/ThesisWork/Ext.agda

@@ -0,0 +1,42 @@
+{-# OPTIONS --cubical #-}
+
+-- Extra stuff not in the cubical standard library
+
+module ThesisWork.Ext where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Function
+open import Cubical.Algebra.Module
+open import Cubical.Algebra.Ring
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+module _ {R : Ring ℓ} where
+  compLeftModule : {M N P : LeftModule R ℓ'}
+    → (f : LeftModuleHom M N)
+    → (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 = 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)
+      pres- x = {!   !}

src/ThesisWork/Graded.agda

@@ -0,0 +1,95 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.Graded where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Algebra.Ring
+open import Cubical.Algebra.Group
+open import Cubical.Algebra.Module
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Foundations.Structure
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+graded : Type ℓ → Type ℓ' → Type (ℓ-max ℓ ℓ')
+graded str I = I → str
+
+GradedModule : Ring ℓ → Type ℓ' → Type (ℓ-max (ℓ-suc ℓ) ℓ')
+GradedModule {ℓ = ℓ} R T = graded (LeftModule R ℓ) T
+
+-- LeftModule homomorphism
+_-[lm]→_ = LeftModuleHom
+
+-- The original definition used an indirect way of defining this to avoid
+-- having to use a transport. Can we do it directly?
+module _ (R : Ring ℓ) (G : Group ℓ') (M₁ M₂ : GradedModule R ⟨ G ⟩) where
+  open RingStr (R .snd) using (_+_; 0r)
+  open GroupStr (G .snd) using (_·_; 1g)
+
+  -- 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
+  record GradedHom : Type (ℓ-max ℓ (ℓ-suc ℓ')) where
+    constructor mkGradedHom
+    field
+      equiv : GroupEquiv G G
+      deg_fn :
+        let e = groupEquivFun equiv in -- the function of the equivalence
+        (g : ⟨ G ⟩) → e g ≡ g · e 1g
+      fn' :
+        let e = groupEquivFun equiv in -- the function of the equivalence
+        {x y : ⟨ G ⟩} → (p : e x ≡ y) → (M₁ x) -[lm]→ (M₂ y)
+
+-- Composition of graded homomorphisms
+gradedHomComp : {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) =
+  mkGradedHom (compGroupEquiv feqv geqv) fgp fgFn where
+    -- Composition of the equivalence
+    fgEqv : ⟨ G ⟩ ≃ ⟨ G ⟩
+    fgEqv = compEquiv (feqv .fst) (geqv .fst)
+
+    open IsGroupHom
+    open GroupStr (G .snd)
+
+    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 =
+      let ff = fp x in -- f(x) ≡ x · f(1g)
+      let gg = gp (f x) in -- g(f(x)) ≡ x · g(f(1g))
+      let p = gg ∙ cong (_· g 1g) (ff ∙ cong (x ·_) (feqv .snd .pres1) ∙ ·IdR x) in
+      let p = p ∙ cong (λ z → x · (g z)) (sym (feqv .snd .pres1)) in
+      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

src/ThesisWork/SpectralSequence.agda

@@ -0,0 +1,43 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.SpectralSequence 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 Cubical.Data.Nat using (ℕ)
+open import Cubical.Data.Int using (ℤ)
+open import Cubical.Data.Sigma
+
+open import ThesisWork.Graded
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+module _ (R : Ring ℓ) where
+  ℤ×ℤGroup = DirProd ℤGroup ℤGroup
+  ℤ×ℤ = ⟨ ℤ×ℤGroup ⟩
+
+  -- As a shorthand, let's make a notation that makes the Ring and Group implicit.
+  _-[gm]→_ : (M₁ M₂ : GradedModule R ℤ×ℤ) → Type (ℓ-max ℓ (ℓ-suc ℓ-zero))
+  _-[gm]→_ M₁ M₂ = GradedHom R ℤ×ℤGroup M₁ M₂
+
+  -- Spectral sequence (definition 5.1.3 in FVD thesis)
+  -- Seems to be https://git.mzhang.io/michael/Spectral/src/commit/2913de520d4fb2c8177a8cbb7e64938291248d03/algebra/spectral_sequence.hlean#L14-L27
+  record SpectralSequence : Type (ℓ-suc ℓ) where
+    field
+      -- A sequence Eᵣ of abelian groups graded over Z × Z for r ≥ 2.
+      -- Eᵣ is called the r-page of the spectral sequence
+      --
+      -- NOTE: Because ℕ starts at zero, I use s = r - 2.
+      E : (s : ℕ) → GradedModule R (ℤ × ℤ)
+
+      -- 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 : ℕ) → ({!   !} ∘ {!   !}) ≡ {!   !}