From aec6a34fb4d23e1103ae6a23bdda12953d1bdea4 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Thu, 2 Jan 2025 10:48:16 -0500 Subject: [PATCH] update --- src/ThesisWork/ExactCouple.agda | 32 +++++++++++++++++++++++ src/ThesisWork/Ext.agda | 7 +++-- src/ThesisWork/Graded.agda | 38 +++++++++++----------------- src/ThesisWork/SpectralSequence.agda | 7 ++--- 4 files changed, 56 insertions(+), 28 deletions(-) create mode 100644 src/ThesisWork/ExactCouple.agda diff --git a/src/ThesisWork/ExactCouple.agda b/src/ThesisWork/ExactCouple.agda new file mode 100644 index 0000000..115e1e0 --- /dev/null +++ b/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 = {! !} \ No newline at end of file diff --git a/src/ThesisWork/Ext.agda b/src/ThesisWork/Ext.agda index 7669f40..500d3d6 100644 --- a/src/ThesisWork/Ext.agda +++ b/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_) diff --git a/src/ThesisWork/Graded.agda b/src/ThesisWork/Graded.agda index 5a9c7a0..a2a46a8 100644 --- a/src/ThesisWork/Graded.agda +++ b/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 \ No newline at end of file diff --git a/src/ThesisWork/SpectralSequence.agda b/src/ThesisWork/SpectralSequence.agda index c237f87..03822cf 100644 --- a/src/ThesisWork/SpectralSequence.agda +++ b/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 : ℕ) → ({! !} ∘ {! !}) ≡ {! !} \ No newline at end of file + dᵣ∘dᵣ≡0 : (s : ℕ) → compGradedModuleHom (d s) (d s) ≡ idGradedModuleHom (E s) + + -- Isomorphisms + -- the cohomology of the cochain complex determined by dᵣ. \ No newline at end of file