Reduced cohomology+Eilenberg-Steenrod axioms

Cubical/Algebra/Group/Instances/Unit.agda

@@ -58,6 +58,23 @@ rightInv (fst rUnitGroupIso) _ = refl
 leftInv (fst rUnitGroupIso) _ = refl
 snd rUnitGroupIso = makeIsGroupHom λ _ _ → refl
 
+-- lifted version
+lUnitGroupIso^ : ∀ {ℓ ℓ'} {G : Group ℓ'}
+  → GroupIso (DirProd (UnitGroup {ℓ}) G) G
+fun (fst lUnitGroupIso^) = snd
+inv (fst lUnitGroupIso^) = tt* ,_
+rightInv (fst lUnitGroupIso^) g = refl
+leftInv (fst lUnitGroupIso^) (tt* , g) = refl
+snd lUnitGroupIso^ = makeIsGroupHom λ _ _ → refl
+
+rUnitGroupIso^ : ∀ {ℓ ℓ'} {G : Group ℓ'}
+  → GroupIso (DirProd G (UnitGroup {ℓ})) G
+fun (fst rUnitGroupIso^) = fst
+inv (fst rUnitGroupIso^) = _, tt*
+rightInv (fst rUnitGroupIso^) g = refl
+leftInv (fst rUnitGroupIso^) (g , tt*) = refl
+snd rUnitGroupIso^ = makeIsGroupHom λ _ _ → refl
+
 lUnitGroupEquiv : {G : Group ℓ} → GroupEquiv (DirProd UnitGroup₀ G) G
 lUnitGroupEquiv = GroupIso→GroupEquiv lUnitGroupIso
 

Cubical/Cohomology/EilenbergMacLane/Base.agda

@@ -4,15 +4,25 @@ module Cubical.Cohomology.EilenbergMacLane.Base where
 
 open import Cubical.Homotopy.EilenbergMacLane.GroupStructure
 open import Cubical.Homotopy.EilenbergMacLane.Base
+open import Cubical.Homotopy.EilenbergMacLane.Properties
 open import Cubical.Homotopy.EilenbergMacLane.Order2
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Pointed.Homogeneous
+open import Cubical.Foundations.Isomorphism
+
+open import Cubical.HITs.PropositionalTruncation as PT
 
 open import Cubical.Data.Nat
+open import Cubical.Data.Sigma
 
 open import Cubical.Algebra.Group.Base
 open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.Morphisms
 open import Cubical.Algebra.AbGroup.Base
 open import Cubical.Algebra.Monoid
 open import Cubical.Algebra.Semigroup
@@ -101,6 +111,163 @@ is-set (isSemigroup (isMonoid (isGroup (isAbGroup (snd (coHomGr n G A)))))) = sq
 ·InvL (isGroup (isAbGroup (snd (coHomGr n G A)))) = lCancelₕ n
 +Comm (isAbGroup (snd (coHomGr n G A))) = commₕ n
 
+-- reduced cohomology groups
+coHomRed : (n : ℕ) (G : AbGroup ℓ) (A : Pointed ℓ') → Type _
+coHomRed n G A = ∥ (A →∙ EM∙ G n) ∥₂
+
+0ₕ∙ : (n : ℕ) {G : AbGroup ℓ} {A : Pointed ℓ'} → coHomRed n G A
+0ₕ∙ n = ∣ (λ _ → 0ₖ n) , refl ∣₂
+
+-- operations
+module _ {n : ℕ} {G : AbGroup ℓ} {A : Pointed ℓ'} where
+  _+ₕ∙_ : coHomRed n G A → coHomRed n G A → coHomRed n G A
+  _+ₕ∙_ = ST.rec2 squash₂
+    λ f g → ∣ (λ x → fst f x +ₖ fst g x)
+            , cong₂ _+ₖ_ (snd f) (snd g) ∙ rUnitₖ n (0ₖ n) ∣₂
+
+  -ₕ∙_ : coHomRed n G A → coHomRed n G A
+  -ₕ∙_ = ST.map λ f → (λ x → -ₖ (fst f x))
+                    , cong -ₖ_ (snd f)
+                    ∙ -0ₖ n
+
+-- group laws
+-- Note that→∙Homogeneous≡ (in Foundations.Pointed.Homogeneous) is
+-- purposely avoided to minimise the size of the proof terms
+module coHomRedAxioms (n : ℕ) {G : AbGroup ℓ} {A : Pointed ℓ'} where
+  commₕ∙ : (x y : coHomRed n G A) → x +ₕ∙ y ≡ y +ₕ∙ x
+  commₕ∙ =
+    ST.elim2 (λ _ _ → isSetPathImplicit)
+      λ f g → cong ∣_∣₂ (ΣPathP (funExt (λ x → commₖ n (fst f x) (fst g x))
+                              , help n _ (sym (snd f)) _ (sym (snd g))))
+    where
+    help : (n : ℕ) (f0 : EM G n) (f1 : 0ₖ n ≡ f0)
+                    (g0 : EM G n) (g1 : 0ₖ n ≡ g0)
+        → PathP (λ i → commₖ n f0 g0 i ≡ 0ₖ n)
+                 (sym (cong₂ _+ₖ_ f1 g1) ∙ rUnitₖ n (0ₖ n))
+                 (sym (cong₂ _+ₖ_ g1 f1) ∙ rUnitₖ n (0ₖ n))
+    help zero _ _ _ _ =
+      isOfHLevelPathP' 0 (is-set (snd G) _ _) _ _ .fst
+    help (suc zero) = J> (J> refl)
+    help (suc (suc n)) = J> (J> refl)
+
+  rCancelₕ∙ : (x : coHomRed n G A) → (x +ₕ∙ (-ₕ∙ x)) ≡ 0ₕ∙ n
+  rCancelₕ∙ =
+    ST.elim (λ _ → isSetPathImplicit)
+      λ f → cong ∣_∣₂ (ΣPathP ((funExt (λ x → rCancelₖ n (fst f x)))
+                    , help n _ (sym (snd f))))
+    where
+    help : (n : ℕ) (f0 : EM G n) (f1 : 0ₖ n ≡ f0)
+      → PathP (λ i → rCancelₖ n f0 i ≡ 0ₖ n)
+               (cong₂ _+ₖ_ (sym f1) (cong -ₖ_ (sym f1) ∙ -0ₖ n)
+                                  ∙ rUnitₖ n (0ₖ n))
+               refl
+    help zero _ _ = isOfHLevelPathP' 0 (is-set (snd G) _ _) _ _ .fst
+    help (suc zero) = J> (sym (rUnit _) ∙ sym (rUnit _))
+    help (suc (suc n)) = J> (sym (rUnit _) ∙ sym (rUnit _))
+
+  lCancelₕ∙ : (x : coHomRed n G A) → ((-ₕ∙ x) +ₕ∙ x) ≡ 0ₕ∙ n
+  lCancelₕ∙ x = commₕ∙ (-ₕ∙ x) x ∙ rCancelₕ∙ x
+
+  rUnitₕ∙ : (x : coHomRed n G A) → (x +ₕ∙ 0ₕ∙ n) ≡ x
+  rUnitₕ∙ = ST.elim (λ _ → isSetPathImplicit)
+     λ f → cong ∣_∣₂ (ΣPathP ((funExt λ x → rUnitₖ n (fst f x))
+                   , help n _ (sym (snd f))))
+    where
+    help : (n : ℕ) (f0 : EM G n) (f1 : 0ₖ n ≡ f0)
+      → PathP (λ i → rUnitₖ n f0 i ≡ 0ₖ n)
+               (cong (_+ₖ 0ₖ n) (sym f1) ∙ rUnitₖ n (0ₖ n))
+               (sym f1)
+    help zero _ _ = isOfHLevelPathP' 0 (is-set (snd G) _ _) _ _ .fst
+    help (suc zero) = J> sym (rUnit refl)
+    help (suc (suc n)) = J> sym (rUnit refl)
+
+  lUnitₕ∙ : (x : coHomRed n G A) → (0ₕ∙ n +ₕ∙ x) ≡ x
+  lUnitₕ∙ = ST.elim (λ _ → isSetPathImplicit)
+    λ f → cong ∣_∣₂ (ΣPathP ((funExt (λ x → lUnitₖ n (fst f x)))
+                  , help n _ (sym (snd f))))
+    where
+    help : (n : ℕ) (f0 : EM G n) (f1 : 0ₖ n ≡ f0)
+      → PathP (λ i → lUnitₖ n f0 i ≡ 0ₖ n)
+               (cong (0ₖ n +ₖ_) (sym f1) ∙ rUnitₖ n (0ₖ n))
+               (sym f1)
+    help zero _ _ = isOfHLevelPathP' 0 (is-set (snd G) _ _) _ _ .fst
+    help (suc zero) = J> sym (rUnit refl)
+    help (suc (suc n)) = J> sym (rUnit refl)
+
+  assocₕ∙ : (x y z : coHomRed n G A) → x +ₕ∙ (y +ₕ∙ z) ≡ (x +ₕ∙ y) +ₕ∙ z
+  assocₕ∙ =
+    ST.elim3 (λ _ _ _ → isSetPathImplicit)
+     λ f g h → cong ∣_∣₂
+       (ΣPathP ((funExt (λ x → assocₖ n (fst f x) (fst g x) (fst h x)))
+      , help n _ (sym (snd f)) _ (sym (snd g)) _ (sym (snd h))))
+    where
+    help : (n : ℕ) (f0 : EM G n) (f1 : 0ₖ n ≡ f0)
+                    (g0 : EM G n) (g1 : 0ₖ n ≡ g0)
+                    (h0 : EM G n) (h1 : 0ₖ n ≡ h0)
+        → PathP (λ i → assocₖ n f0 g0 h0 i ≡ 0ₖ n)
+                 (cong₂ _+ₖ_ (sym f1)
+                  (cong₂ _+ₖ_ (sym g1) (sym h1) ∙ rUnitₖ n (0ₖ n))
+                    ∙ rUnitₖ n (0ₖ n))
+                 (cong₂ _+ₖ_ (cong₂ _+ₖ_ (sym f1) (sym g1)
+                   ∙ rUnitₖ n (0ₖ n)) (sym h1) ∙ rUnitₖ n (0ₖ n))
+    help zero _ _ _ _ _ _ = isOfHLevelPathP' 0 (is-set (snd G) _ _) _ _ .fst
+    help (suc zero) =
+      J> (J> (J> cong (_∙ refl)
+        (cong (cong₂ _+ₖ_ refl) (sym (rUnit refl))
+        ∙ (cong (λ z → cong₂ (+ₖ-syntax {G = G} 1) z (refl {x = 0ₖ {G = G} 1}))
+          (rUnit refl)))))
+    help (suc (suc n)) =
+      J> (J> (J> flipSquare ((sym (rUnit refl))
+        ◁ flipSquare (cong (_∙ refl)
+        (cong (cong₂ _+ₖ_ refl) (sym (rUnit refl))
+        ∙ (cong (λ z → cong₂ (+ₖ-syntax {G = G} (suc (suc n))) z
+                              (refl {x = 0ₖ {G = G} (suc (suc n))}))
+          (rUnit refl)))))))
+
+coHomRedGr : (n : ℕ) (G : AbGroup ℓ) (A : Pointed ℓ') → AbGroup _
+fst (coHomRedGr n G A) = coHomRed n G A
+0g (snd (coHomRedGr n G A)) = 0ₕ∙ n
+AbGroupStr._+_ (snd (coHomRedGr n G A)) = _+ₕ∙_
+- snd (coHomRedGr n G A) = -ₕ∙_
+is-set (isSemigroup (isMonoid (isGroup (isAbGroup (snd (coHomRedGr n G A)))))) = squash₂
+·Assoc (isSemigroup (isMonoid (isGroup (isAbGroup (snd (coHomRedGr n G A)))))) = coHomRedAxioms.assocₕ∙ n
+·IdR (isMonoid (isGroup (isAbGroup (snd (coHomRedGr n G A))))) = coHomRedAxioms.rUnitₕ∙ n
+·IdL (isMonoid (isGroup (isAbGroup (snd (coHomRedGr n G A))))) = coHomRedAxioms.lUnitₕ∙ n
+·InvR (isGroup (isAbGroup (snd (coHomRedGr n G A)))) = coHomRedAxioms.rCancelₕ∙ n
+·InvL (isGroup (isAbGroup (snd (coHomRedGr n G A)))) = coHomRedAxioms.lCancelₕ∙ n
++Comm (isAbGroup (snd (coHomRedGr n G A))) = coHomRedAxioms.commₕ∙ n
+
+coHom≅coHomRed : (n : ℕ) (G : AbGroup ℓ) (A : Pointed ℓ')
+  → AbGroupEquiv (coHomGr (suc n) G (fst A)) (coHomRedGr (suc n) G A)
+coHom≅coHomRed n G A =
+  GroupIso→GroupEquiv (invGroupIso main)
+  where
+  con-lem : (n : ℕ) (x : EM G (suc n)) → ∥ x ≡ 0ₖ (suc n) ∥₁
+  con-lem n =
+    EM-raw'-elim G (suc n)
+     (λ _ → isProp→isOfHLevelSuc (suc n) squash₁)
+       (EM-raw'-trivElim G n (λ _ → isProp→isOfHLevelSuc n squash₁)
+         ∣ EM-raw'→EM∙ G (suc n) ∣₁)
+
+  main : GroupIso _ _
+  Iso.fun (fst main) = ST.map fst
+  Iso.inv (fst main) = ST.map λ f → (λ x → f x -ₖ f (pt A))
+                            , rCancelₖ (suc n) (f (pt A))
+  Iso.rightInv (fst main) =
+    ST.elim (λ _ → isSetPathImplicit)
+      λ f → PT.rec (squash₂ _ _)
+        (λ p → cong ∣_∣₂
+          (funExt λ x → cong (λ z → f x +ₖ z)
+            (cong -ₖ_ p ∙ -0ₖ (suc n)) ∙ rUnitₖ (suc n) (f x)))
+        (con-lem n (f (pt A)))
+  Iso.leftInv (fst main) =
+    ST.elim (λ _ → isSetPathImplicit)
+      λ f → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM (suc n))
+             (funExt λ x → cong (fst f x +ₖ_) (cong -ₖ_ (snd f) ∙ -0ₖ (suc n))
+                          ∙ rUnitₖ (suc n) (fst f x)))
+  snd main =
+    makeIsGroupHom (ST.elim2 (λ _ _ → isSetPathImplicit)
+      λ _ _ → refl)
 
 -- ℤ/2 lemmas
 +ₕ≡id-ℤ/2 : ∀ {ℓ}  {A : Type ℓ} (n : ℕ) (x : coHom n ℤ/2 A) → x +ₕ x ≡ 0ₕ n
@@ -128,3 +295,16 @@ fst (coHomHom n f) = coHomFun n f
 snd (coHomHom n f) =
   makeIsGroupHom (ST.elim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _)
    λ f g → refl)
+
+coHomFun∙ : ∀ {ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {G : AbGroup ℓ''}
+            (n : ℕ) (f : A →∙ B)
+         → coHomRed n G B → coHomRed n G A
+coHomFun∙ n f = ST.map λ g → g ∘∙ f
+
+coHomHom∙ : ∀ {ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {G : AbGroup ℓ''}
+            (n : ℕ) (f : A →∙ B)
+         → AbGroupHom (coHomRedGr n G B) (coHomRedGr n G A)
+fst (coHomHom∙ n f) = coHomFun∙ n f
+snd (coHomHom∙ n f) =
+  makeIsGroupHom (ST.elim2 (λ _ _ → isSetPathImplicit)
+    λ g h → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl))