From 953e80c3b1f42d1f45db87ffd71f60a3fa4b9790 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Mon, 30 Dec 2024 15:21:12 -0500 Subject: [PATCH] wip --- .vscode/settings.json | 1 - src/AOP/Focus.agda | 20 ++++-- src/ThesisWork/Ext.agda | 42 ++++++++++++ src/ThesisWork/Graded.agda | 95 ++++++++++++++++++++++++++++ src/ThesisWork/SpectralSequence.agda | 43 +++++++++++++ 5 files changed, 195 insertions(+), 6 deletions(-) create mode 100644 src/ThesisWork/Ext.agda create mode 100644 src/ThesisWork/Graded.agda create mode 100644 src/ThesisWork/SpectralSequence.agda diff --git a/.vscode/settings.json b/.vscode/settings.json index 6cab46b..73a3e49 100644 --- a/.vscode/settings.json +++ b/.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" } diff --git a/src/AOP/Focus.agda b/src/AOP/Focus.agda index 2c0327f..3de2367 100644 --- a/src/AOP/Focus.agda +++ b/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)) \ No newline at end of file + 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)) \ No newline at end of file diff --git a/src/ThesisWork/Ext.agda b/src/ThesisWork/Ext.agda new file mode 100644 index 0000000..8be464e --- /dev/null +++ b/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 = {! !} \ No newline at end of file diff --git a/src/ThesisWork/Graded.agda b/src/ThesisWork/Graded.agda new file mode 100644 index 0000000..c6c4121 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/src/ThesisWork/SpectralSequence.agda b/src/ThesisWork/SpectralSequence.agda new file mode 100644 index 0000000..c237f87 --- /dev/null +++ b/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 : ℕ) → ({! !} ∘ {! !}) ≡ {! !} \ No newline at end of file