H*(Kleinbottle,Z/2)

Cubical/Algebra/Group/Instances/IntMod.agda

@@ -207,5 +207,11 @@ isHomℤ→Fin n =
 ℤ/2-elim {A = A} a₀ a₁ (suc (suc x) , p) =
   ⊥.rec (snotz (cong (λ x → predℕ (predℕ x)) (+-comm (3 +ℕ x) (fst p) ∙ snd p)))
 
+ℤ/2-rec : ∀ {ℓ} {A : Type ℓ} → A → A → Fin 2 → A
+ℤ/2-rec {A = A} a₀ a₁ (zero , p) = a₀
+ℤ/2-rec {A = A} a₀ a₁ (suc zero , p) = a₁
+ℤ/2-rec {A = A} a₀ a₁ (suc (suc x) , p) =
+  ⊥.rec (snotz (cong (λ x → predℕ (predℕ x)) (+-comm (3 +ℕ x) (fst p) ∙ snd p)))
+
 -Const-ℤ/2 : (x : fst (ℤGroup/ 2)) → -ₘ x ≡ x
 -Const-ℤ/2 = ℤ/2-elim refl refl

Cubical/Cohomology/EilenbergMacLane/Base.agda

@@ -4,6 +4,7 @@ module Cubical.Cohomology.EilenbergMacLane.Base where
 
 open import Cubical.Homotopy.EilenbergMacLane.GroupStructure
 open import Cubical.Homotopy.EilenbergMacLane.Base
+open import Cubical.Homotopy.EilenbergMacLane.Order2
 
 open import Cubical.Foundations.Prelude
 
@@ -13,6 +14,7 @@ open import Cubical.Algebra.Group.Base
 open import Cubical.Algebra.AbGroup.Base
 open import Cubical.Algebra.Monoid
 open import Cubical.Algebra.Semigroup
+open import Cubical.Algebra.Group.Instances.IntMod
 
 open import Cubical.HITs.SetTruncation as ST
   hiding (rec ; map ; elim ; elim2 ; elim3)
@@ -96,3 +98,18 @@ is-set (isSemigroup (isMonoid (isGroup (isAbGroup (snd (coHomGr n G A)))))) = sq
 ·InvR (isGroup (isAbGroup (snd (coHomGr n G A)))) = rCancelₕ n
 ·InvL (isGroup (isAbGroup (snd (coHomGr n G A)))) = lCancelₕ n
 +Comm (isAbGroup (snd (coHomGr n G A))) = commₕ n
+
+
+-- ℤ/2 lemmas
++ₕ≡id-ℤ/2 : ∀ {ℓ}  {A : Type ℓ} (n : ℕ) (x : coHom n ℤ/2 A) → x +ₕ x ≡ 0ₕ n
++ₕ≡id-ℤ/2 n =
+  ST.elim (λ _ → isSetPathImplicit)
+    λ f → cong ∣_∣₂ (funExt λ x → +ₖ≡id-ℤ/2 n (f x))
+
+-ₕConst-ℤ/2 : ∀{ℓ} (n : ℕ) {A : Type ℓ} (x : coHom n ℤ/2 A) → -ₕ x ≡ x
+-ₕConst-ℤ/2 zero =
+  ST.elim (λ _ → isSetPathImplicit)
+    λ f → cong ∣_∣₂ (funExt λ x → -Const-ℤ/2 (f x))
+-ₕConst-ℤ/2 (suc n) =
+  ST.elim (λ _ → isSetPathImplicit)
+    λ f → cong ∣_∣₂ (funExt λ x → -ₖConst-ℤ/2 n (f x))

Cubical/Cohomology/EilenbergMacLane/CupProduct.agda

@@ -14,6 +14,7 @@ open import Cubical.Algebra.Ring
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Transport
 
 open import Cubical.HITs.EilenbergMacLane1
 open import Cubical.HITs.SetTruncation as ST
@@ -93,3 +94,19 @@ module _ {G'' : Ring ℓ} {A : Type ℓ'} where
           λ h → cong ∣_∣₂ (funExt λ x → assoc⌣ₖ n m l (f x) (g x) (h x)
             ∙ cong (transport (λ i → EM G' (+'-assoc n m l i)))
                (cong (λ x → (f x ⌣ₖ (g x ⌣ₖ h x))) (sym (transportRefl x))))
+
+-- dependent versions
+module _ {G'' : Ring ℓ} {A : Type ℓ'} where
+  private
+    G' = Ring→AbGroup G''
+
+  ⌣-1ₕDep : (n : ℕ) (x : coHom n G' A)
+    → PathP (λ i → coHom (+'-comm zero n (~ i)) G' A) (x ⌣ 1ₕ) x
+  ⌣-1ₕDep n x = toPathP {A = λ i → coHom (+'-comm zero n (~ i)) G' A}
+                        (flipTransport (⌣-1ₕ n x))
+
+  assoc⌣Dep : (n m l : ℕ)
+       (x : coHom n G' A) (y : coHom m G' A) (z : coHom l G' A)
+    → PathP (λ i → coHom (+'-assoc n m l (~ i)) G' A) ((x ⌣ y) ⌣ z) (x ⌣ (y ⌣ z))
+  assoc⌣Dep n m l x y z = toPathP {A = λ i → coHom (+'-assoc n m l (~ i)) G' A}
+                                  (flipTransport (assoc⌣ n m l x y z))

Cubical/Cohomology/EilenbergMacLane/Groups/KleinBottle.agda

@@ -335,26 +335,27 @@ snd H²[K²,ℤ/2]≅ℤ/2 =
         (ℤ/2-elim (IsAbGroup.+IdR e 1)
           (IsAbGroup.+InvR e 1))))
 
+isContr-HⁿKleinBottle : (n : ℕ) (G : AbGroup ℓ)
+  → isContr (coHom (suc (suc (suc n))) G KleinBottle)
+fst (isContr-HⁿKleinBottle n G) = ∣ (KleinFun ∣ north ∣ refl refl refl) ∣₂
+snd (isContr-HⁿKleinBottle n G) = ST.elim (λ _ → isSetPathImplicit)
+         (ConnK².elim₂ (isConnectedSubtr 3 (suc n)
+           (subst (λ m → isConnected m (EM G (3 +ℕ n)))
+             (cong suc (+-comm 3 n))
+             (isConnectedEM (3 +ℕ n)))) (λ _ → squash₂ _ _)
+            (0ₖ (3 +ℕ n))
+            λ p → TR.rec (squash₂ _ _)
+              (λ q → cong ∣_∣₂ (cong (KleinFun ∣ north ∣ refl refl) q))
+              (isConnectedPath 1
+                (isConnectedPath 2
+                  (isConnectedPath 3
+                    ((isConnectedSubtr 4 n
+                     (subst (λ m → isConnected m (EM G (3 +ℕ n)))
+                       (+-comm 4 n)
+                       (isConnectedEM (3 +ℕ n))))) _ _) _ _)
+                         refl p .fst))
+
 H³⁺ⁿK²≅0 : (n : ℕ) (G : AbGroup ℓ)
   → AbGroupEquiv (coHomGr (3 +ℕ n) G KleinBottle) (trivialAbGroup {ℓ})
-fst (H³⁺ⁿK²≅0 n G) = isContr→Equiv lem isContrUnit*
-  where
-  lem : isContr (coHom (suc (suc (suc n))) G KleinBottle)
-  fst lem = ∣ (KleinFun ∣ north ∣ refl refl refl) ∣₂
-  snd lem = ST.elim (λ _ → isSetPathImplicit)
-           (ConnK².elim₂ (isConnectedSubtr 3 (suc n)
-             (subst (λ m → isConnected m (EM G (3 +ℕ n)))
-               (cong suc (+-comm 3 n))
-               (isConnectedEM (3 +ℕ n)))) (λ _ → squash₂ _ _)
-              (0ₖ (3 +ℕ n))
-              λ p → TR.rec (squash₂ _ _)
-                (λ q → cong ∣_∣₂ (cong (KleinFun ∣ north ∣ refl refl) q))
-                (isConnectedPath 1
-                  (isConnectedPath 2
-                    (isConnectedPath 3
-                      ((isConnectedSubtr 4 n
-                       (subst (λ m → isConnected m (EM G (3 +ℕ n)))
-                         (+-comm 4 n)
-                         (isConnectedEM (3 +ℕ n))))) _ _) _ _)
-                           refl p .fst))
+fst (H³⁺ⁿK²≅0 n G) = isContr→Equiv (isContr-HⁿKleinBottle n G) isContrUnit*
 snd (H³⁺ⁿK²≅0 n G) = makeIsGroupHom λ _ _ → refl

Cubical/Cohomology/EilenbergMacLane/Groups/Wedge.agda

@@ -0,0 +1,128 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Cohomology.EilenbergMacLane.Groups.Wedge where
+
+open import Cubical.Cohomology.EilenbergMacLane.Base
+
+open import Cubical.Homotopy.EilenbergMacLane.Base
+open import Cubical.Homotopy.EilenbergMacLane.GroupStructure
+open import Cubical.Homotopy.EilenbergMacLane.Properties
+open import Cubical.Homotopy.Connected
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Function
+
+open import Cubical.Data.Nat
+open import Cubical.Data.Sigma
+
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.Properties
+open import Cubical.Algebra.AbGroup.Base
+
+open import Cubical.HITs.SetTruncation as ST
+open import Cubical.HITs.Truncation as Trunc
+open import Cubical.HITs.Pushout
+open import Cubical.HITs.Wedge
+
+open import Cubical.Foundations.HLevels
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module _ {A : Pointed ℓ} {B : Pointed ℓ'} (G : AbGroup ℓ) where
+  A∨B = A ⋁ B
+
+  open AbGroupStr (snd G) renaming (_+_ to _+G_ ; -_ to -G_)
+
+  private
+    ×H : (n : ℕ) → AbGroup _
+    ×H n = dirProdAb (coHomGr (suc n) G (fst A))
+                     (coHomGr (suc n) G (fst B))
+
+  Hⁿ×→Hⁿ-⋁ : (n : ℕ) → (A ⋁ B → EM G (suc n))
+    → (fst A → EM G (suc n)) × (fst B → EM G (suc n))
+  fst (Hⁿ×→Hⁿ-⋁ n f) x = f (inl x)
+  snd (Hⁿ×→Hⁿ-⋁ n f) x = f (inr x)
+
+  Hⁿ-⋁→Hⁿ× : (n : ℕ)
+    → (f : fst A → EM G (suc n))
+    → (g : fst B → EM G (suc n))
+    → (A ⋁ B → EM G (suc n))
+  Hⁿ-⋁→Hⁿ× n f g (inl x) = f x -[ (suc n) ]ₖ f (pt A)
+  Hⁿ-⋁→Hⁿ× n f g (inr x) = g x -[ (suc n) ]ₖ g (pt B)
+  Hⁿ-⋁→Hⁿ× n f g (push a i) =
+    (rCancelₖ (suc n) (f (pt A)) ∙ sym (rCancelₖ (suc n) (g (pt B)))) i
+
+  Hⁿ⋁-Iso : (n : ℕ)
+    → Iso (coHom (suc n) G (A ⋁ B))
+           (coHom (suc n) G (fst A)
+          × coHom (suc n) G (fst B))
+  Iso.fun (Hⁿ⋁-Iso n) =
+    ST.rec (isSet× squash₂ squash₂)
+      λ f → ∣ f ∘ inl ∣₂ , ∣ f ∘ inr ∣₂
+  Iso.inv (Hⁿ⋁-Iso n) =
+    uncurry (ST.rec2 squash₂ λ f g → ∣ Hⁿ-⋁→Hⁿ× n f g ∣₂)
+  Iso.rightInv (Hⁿ⋁-Iso n) =
+    uncurry (ST.elim2
+      (λ _ _ → isOfHLevelPath 2 (isSet× squash₂ squash₂) _ _)
+      λ f g
+      → ΣPathP (Trunc.rec (isProp→isOfHLevelSuc n (squash₂ _ _))
+                (λ p → cong ∣_∣₂ (funExt λ x → cong (λ z → f x +[ (suc n) ]ₖ z)
+                                 (cong (λ z → -[ (suc n) ]ₖ z) p ∙ -0ₖ (suc n))
+                              ∙ rUnitₖ (suc n) (f x)))
+              (isConnectedPath (suc n)
+               (isConnectedEM (suc n)) (f (pt A)) (0ₖ (suc n)) .fst)
+            , Trunc.rec (isProp→isOfHLevelSuc n (squash₂ _ _))
+                (λ p → cong ∣_∣₂ (funExt λ x → cong (λ z → g x +[ (suc n) ]ₖ z)
+                                 (cong (λ z → -[ (suc n) ]ₖ z) p ∙ -0ₖ (suc n))
+                              ∙ rUnitₖ (suc n) (g x)))
+              (isConnectedPath (suc n)
+               (isConnectedEM (suc n)) (g (pt B)) (0ₖ (suc n)) .fst)))
+  Iso.leftInv (Hⁿ⋁-Iso n) =
+    ST.elim (λ _ → isSetPathImplicit)
+      λ f → Trunc.rec (isProp→isOfHLevelSuc n (squash₂ _ _))
+        (λ p → cong ∣_∣₂
+          (funExt λ { (inl x) → pgen f p (inl x)
+                    ; (inr x) → p₂ f p x
+                    ; (push a i) j → Sq f p j i}))
+        (Iso.fun (PathIdTruncIso (suc n))
+          (isContr→isProp (isConnectedEM {G' = G}  (suc n))
+            ∣ f (inl (pt A)) ∣ ∣ 0ₖ (suc n) ∣ ))
+    where
+    module _ (f : (A ⋁ B → EM G (suc n))) (p : f (inl (pt A)) ≡ 0ₖ (suc n))
+      where
+      pgen : (x : A ⋁ B) → _ ≡ _
+      pgen x =
+          (λ j → f x -[ (suc n) ]ₖ (p j))
+       ∙∙ (λ j → f x +[ (suc n) ]ₖ (-0ₖ (suc n) j))
+       ∙∙ rUnitₖ (suc n) (f x)
+
+      p₂ : (x : typ B) → _ ≡ _
+      p₂ x = (λ j → f (inr x) -[ (suc n) ]ₖ (f (sym (push tt) j)))
+            ∙ pgen (inr x)
+
+
+      Sq : Square (rCancelₖ (suc n) (f (inl (pt A)))
+                    ∙ sym (rCancelₖ (suc n) (f (inr (pt B)))))
+                   (cong f (push tt))
+                   (pgen (inl (pt A)))
+                   (p₂ (pt B))
+      Sq i j =
+        hcomp (λ k → λ {(i = i0) → (rCancelₖ (suc n) (f (inl (pt A)))
+                                   ∙ sym (rCancelₖ (suc n) (f (push tt k)))) j
+                       ; (i = i1) → f (push tt (k ∧ j))
+                       ; (j = i0) → pgen (inl (pt A)) i
+                       ; (j = i1) → ((λ j → f (push tt k) -[ (suc n) ]ₖ
+                                             (f (sym (push tt) (j ∨ ~ k))))
+                                    ∙ pgen (push tt k)) i})
+         (hcomp (λ k → λ {(i = i0) → rCancel (rCancelₖ (suc n)
+                                               (f (inl (pt A)))) (~ k) j
+                         ; (i = i1) → f (inl (pt A))
+                         ; (j = i0) → pgen (inl (pt A)) i
+                         ; (j = i1) → lUnit (pgen (inl (pt A))) k i})
+                (pgen (inl (pt A)) i))