Deploying to gh-pages from @ c6a96ee 🚀

agda · Feb 2, 2024 · 9b5a1cf · 9b5a1cf
1 parent cdca427
commit 9b5a1cf
Show file tree

Hide file tree

Showing 8 changed files with 1,189 additions and 15 deletions.
diff --git a/Cubical.Experiments.CohomologyGroups.html b/Cubical.Experiments.CohomologyGroups.html
@@ -0,0 +1,143 @@
+<!DOCTYPE HTML>
+<html><head><meta charset="utf-8"><title>Cubical.Experiments.CohomologyGroups</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--safe</a> <a id="20" class="Symbol">#-}</a>
+<a id="24" class="Keyword">module</a> <a id="31" href="Cubical.Experiments.CohomologyGroups.html" class="Module">Cubical.Experiments.CohomologyGroups</a> <a id="68" class="Keyword">where</a>
+<a id="74" class="Comment">{-
+open import Cubical.Experiments.ZCohomologyOld.Base
+open import Cubical.Experiments.ZCohomologyOld.Properties
+open import Cubical.Experiments.ZCohomologyOld.MayerVietorisUnreduced
+open import Cubical.Experiments.ZCohomologyOld.Groups.Unit
+open import Cubical.Experiments.ZCohomologyOld.KcompPrelims
+open import Cubical.Experiments.ZCohomologyOld.Groups.Sn
+
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Isomorphism
+
+open import Cubical.HITs.Pushout
+open import Cubical.HITs.Sn
+open import Cubical.HITs.SetTruncation
+  renaming (rec to sRec ; elim to sElim ; elim2 to sElim2)
+  hiding (map)
+open import Cubical.HITs.PropositionalTruncation
+  renaming (rec to pRec ; ∥_∥ to ∥_∥₁ ; ∣_∣ to ∣_∣₁)
+  hiding (map)
+
+open import Cubical.Data.Bool
+open import Cubical.Data.Sigma
+open import Cubical.Data.Int
+
+open import Cubical.Algebra.Group
+
+open GroupIso
+open GroupHom
+open BijectionIso
+
+-- --------------------------H¹(S¹) -----------------------------------
+{-
+In order to apply Mayer-Vietoris, we need the following lemma.
+Given the following diagram
+  a ↦ (a , 0)   ψ         ϕ
+ A --&gt;  A × A -------&gt; B ---&gt;  C
+If ψ is an isomorphism and ϕ is surjective with ker ϕ ≡ {ψ (a , a) ∣ a ∈ A}, then C ≅ B
+-}
+
+
+diagonalIso : ∀ {ℓ ℓ&#39; ℓ&#39;&#39;} {A : Group {ℓ}} (B : Group {ℓ&#39;}) {C : Group {ℓ&#39;&#39;}}
+               (ψ : GroupIso (dirProd A A) B) (ϕ : GroupHom B C)
+             → isSurjective _ _ ϕ
+             → ((x : ⟨ B ⟩) → isInKer B C ϕ x
+                                    → ∃[ y ∈ ⟨ A ⟩ ] x ≡ (fun (map ψ)) (y , y))
+             → ((x : ⟨ B ⟩) → (∃[ y ∈ ⟨ A ⟩ ] x ≡ (fun (map ψ)) (y , y))
+                                    → isInKer B C ϕ x)
+             → GroupIso A C
+diagonalIso {A = A} B {C = C} ψ ϕ issurj ker→diag diag→ker = BijectionIsoToGroupIso bijIso
+  where
+  open GroupStr
+  module A = GroupStr (snd A)
+  module B = GroupStr (snd B)
+  module C = GroupStr (snd C)
+  module A×A = GroupStr (snd (dirProd A A))
+  module ψ = GroupIso ψ
+  module ϕ = GroupHom ϕ
+  ψ⁻ = inv ψ
+
+  fstProj : GroupHom A (dirProd A A)
+  fun fstProj a = a , GroupStr.0g (snd A)
+  isHom fstProj g0 g1 i = (g0 A.+ g1) , GroupStr.lid (snd A) (GroupStr.0g (snd A)) (~ i)
+
+  bijIso : BijectionIso A C
+  map&#39; bijIso = compGroupHom fstProj (compGroupHom (map ψ) ϕ)
+  inj bijIso a inker = pRec (isSetCarrier A _ _)
+                             (λ {(a&#39; , id) → (cong fst (sym (leftInv ψ (a , GroupStr.0g (snd A))) ∙∙ cong ψ⁻ id ∙∙ leftInv ψ (a&#39; , a&#39;)))
+                                           ∙ cong snd (sym (leftInv ψ (a&#39; , a&#39;)) ∙∙ cong ψ⁻ (sym id) ∙∙ leftInv ψ (a , GroupStr.0g (snd A)))})
+                             (ker→diag _ inker)
+  surj bijIso c =
+    pRec isPropPropTrunc
+         (λ { (b , id) → ∣ (fst (ψ⁻ b) A.+ (A.- snd (ψ⁻ b)))
+                          , ((sym (GroupStr.rid (snd C) _)
+                           ∙∙ cong ((fun ϕ) ((fun (map ψ)) (fst (ψ⁻ b) A.+ (A.- snd (ψ⁻ b)) , GroupStr.0g (snd A))) C.+_)
+                                  (sym (diag→ker (fun (map ψ) ((snd (ψ⁻ b)) , (snd (ψ⁻ b))))
+                                                  ∣ (snd (ψ⁻ b)) , refl ∣₁))
+                           ∙∙ sym ((isHom ϕ) _ _))
+                           ∙∙ cong (fun ϕ) (sym ((isHom (map ψ)) _ _)
+                                        ∙∙ cong (fun (map ψ)) (ΣPathP (sym (GroupStr.assoc (snd A) _ _ _)
+                                                                           ∙∙ cong (fst (ψ⁻ b) A.+_) (GroupStr.invl (snd A) _)
+                                                                           ∙∙ GroupStr.rid (snd A) _
+                                                                        , (GroupStr.lid (snd A) _)))
+                                        ∙∙ rightInv ψ b)
+                           ∙∙ id) ∣₁ })
+         (issurj c)
+
+H¹-S¹≅ℤ : GroupIso intGroup (coHomGr 1 (S₊ 1))
+H¹-S¹≅ℤ =
+    diagonalIso (coHomGr 0 (S₊ 0))
+                (invGroupIso H⁰-S⁰≅ℤ×ℤ)
+                (K.d 0)
+                (λ x → K.Ker-i⊂Im-d 0 x
+                                     (ΣPathP (isOfHLevelSuc 0 (isContrHⁿ-Unit 0) _ _
+                                            , isOfHLevelSuc 0 (isContrHⁿ-Unit 0) _ _)))
+                ((sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 isPropPropTrunc)
+                        (λ x inker
+                            → pRec isPropPropTrunc
+                                    (λ {((f , g) , id&#39;) → helper x f g id&#39; inker})
+                                    ((K.Ker-d⊂Im-Δ 0 ∣ x ∣₂ inker)))))
+                ((sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelPath 2 isSetSetTrunc _ _)
+                         λ F surj
+                           → pRec (isSetSetTrunc _ _)
+                                   (λ { (x , id) → K.Im-Δ⊂Ker-d 0 ∣ F ∣₂
+                                                      ∣ (∣ (λ _ → x) ∣₂ , ∣ (λ _ → 0) ∣₂) ,
+                                                       (cong ∣_∣₂ (funExt (surjHelper x))) ∙ sym id ∣₁ })
+                                   surj) )
+  □ invGroupIso (coHomPushout≅coHomSn 0 1)
+  where
+  module K = MV Unit Unit (S₊ 0) (λ _ → tt) (λ _ → tt)
+
+  surjHelper :  (x : Int) (x₁ : S₊ 0) → x -[ 0 ]ₖ 0 ≡ S0→Int (x , x) x₁
+  surjHelper x true = Iso.leftInv (Iso-Kn-ΩKn+1 0) x
+  surjHelper x false = Iso.leftInv (Iso-Kn-ΩKn+1 0) x
+
+  helper : (F : S₊ 0 → Int) (f g : ∥ (Unit → Int) ∥₂)
+           (id : GroupHom.fun (K.Δ 0) (f , g) ≡ ∣ F ∣₂)
+         → isInKer (coHomGr 0 (S₊ 0))
+                    (coHomGr 1 (Pushout (λ _ → tt) (λ _ → tt)))
+                    (K.d 0)
+                    ∣ F ∣₂
+         → ∃[ x ∈ Int ] ∣ F ∣₂ ≡ inv H⁰-S⁰≅ℤ×ℤ (x , x)
+  helper F =
+    sElim2 (λ _ _ → isOfHLevelΠ 2 λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 isPropPropTrunc)
+           λ f g id inker
+             → pRec isPropPropTrunc
+                     (λ ((a , b) , id2)
+                        → sElim2 {C = λ f g → GroupHom.fun (K.Δ 0) (f , g) ≡ ∣ F ∣₂ → _ }
+                                  (λ _ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 isPropPropTrunc)
+                                  (λ f g id → ∣ (helper2 f g .fst) , (sym id ∙ sym (helper2 f g .snd)) ∣₁)
+                                  a b id2)
+                     (MV.Ker-d⊂Im-Δ _ _ (S₊ 0) (λ _ → tt) (λ _ → tt) 0 ∣ F ∣₂ inker)
+    where
+    helper2 : (f g : Unit → Int)
+            → Σ[ x ∈ Int ] (inv H⁰-S⁰≅ℤ×ℤ (x , x))
+             ≡ GroupHom.fun (K.Δ 0) (∣ f ∣₂ , ∣ g ∣₂)
+    helper2 f g = (f _ -[ 0 ]ₖ g _) , cong ∣_∣₂ (funExt λ {true → refl ; false → refl})
+-}</a>
+</pre></body></html>