Summary file/missing cohomology lemmas

Cubical/Algebra/AbGroup/Base.agda

@@ -315,10 +315,6 @@ module _ {ℓ ℓ' : Level} (AGr : Group ℓ) (BGr : AbGroup ℓ') where
       renaming (_·_ to _∙A_ ; inv to -A_
                 ; 1g to 1A ; ·IdR to ·IdRA)
 
-  trivGroupHom : GroupHom AGr (BGr *)
-  fst trivGroupHom x = 0B
-  snd trivGroupHom = makeIsGroupHom λ _ _ → sym (+IdRB 0B)
-
   compHom : GroupHom AGr (BGr *) → GroupHom AGr (BGr *) → GroupHom AGr (BGr *)
   fst (compHom f g) x = fst f x +B fst g x
   snd (compHom f g) =

Cubical/Algebra/AbGroup/Instances/DirectProduct.agda

@@ -0,0 +1,15 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.AbGroup.Instances.DirectProduct where
+
+open import Cubical.Data.Sigma
+open import Cubical.Algebra.AbGroup.Base
+open import Cubical.Algebra.Group.DirProd
+
+AbDirProd : ∀ {ℓ ℓ'} → AbGroup ℓ → AbGroup ℓ' → AbGroup (ℓ-max ℓ ℓ')
+AbDirProd G H =
+  Group→AbGroup (DirProd (AbGroup→Group G) (AbGroup→Group H)) comm
+  where
+  comm : (x y : fst G × fst H) → _ ≡ _
+  comm (g1 , h1) (g2 , h2) =
+    ΣPathP (AbGroupStr.+Comm (snd G) g1 g2
+          , AbGroupStr.+Comm (snd H) h1 h2)

Cubical/Algebra/AbGroup/Instances/Int.agda

@@ -0,0 +1,11 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.AbGroup.Instances.Int where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Int
+open import Cubical.Algebra.AbGroup.Base
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Group.Instances.Int
+
+ℤAbGroup : AbGroup ℓ-zero
+ℤAbGroup = Group→AbGroup ℤGroup +Comm

Cubical/Algebra/AbGroup/Instances/IntMod.agda

@@ -0,0 +1,89 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.AbGroup.Instances.IntMod where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Function
+
+open import Cubical.Algebra.AbGroup
+
+open import Cubical.Algebra.Group.Instances.Int
+open import Cubical.Algebra.AbGroup.Instances.Int
+open import Cubical.Algebra.Group.Instances.IntMod
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.ZAction
+
+open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Nat renaming (_+_ to _+ℕ_ ; _·_ to _·ℕ_)
+open import Cubical.Data.Nat.Order
+open import Cubical.Data.Int
+  renaming (_+_ to _+ℤ_ ; _·_ to _·ℤ_ ; -_ to -ℤ_)
+open import Cubical.Data.Fin
+open import Cubical.Data.Fin.Arithmetic
+open import Cubical.Data.Sigma
+
+open import Cubical.HITs.SetQuotients as SQ
+open import Cubical.HITs.PropositionalTruncation as PT
+
+ℤAbGroup/_ : ℕ → AbGroup ℓ-zero
+ℤAbGroup/ n = Group→AbGroup (ℤGroup/ n) (comm n)
+  where
+  comm : (n : ℕ) (x y : fst (ℤGroup/ n))
+   → GroupStr._·_ (snd (ℤGroup/ n)) x y
+    ≡ GroupStr._·_ (snd (ℤGroup/ n)) y x
+  comm zero = +Comm
+  comm (suc n) = +ₘ-comm
+
+ℤ/2 : AbGroup ℓ-zero
+ℤ/2 = ℤAbGroup/ 2
+
+ℤ/2[2]≅ℤ/2 : AbGroupIso (ℤ/2 [ 2 ]ₜ) ℤ/2
+Iso.fun (fst ℤ/2[2]≅ℤ/2) = fst
+Iso.inv (fst ℤ/2[2]≅ℤ/2) x = x , cong (x +ₘ_) (+ₘ-rUnit x) ∙ x+x x
+  where
+  x+x : (x : ℤ/2 .fst) → x +ₘ x ≡ fzero
+  x+x = ℤ/2-elim refl refl
+Iso.rightInv (fst ℤ/2[2]≅ℤ/2) x = Σ≡Prop (λ _ → isProp≤) refl
+Iso.leftInv (fst ℤ/2[2]≅ℤ/2) x = Σ≡Prop (λ _ → isSetFin _ _) refl
+snd ℤ/2[2]≅ℤ/2 = makeIsGroupHom λ _ _ → refl
+
+ℤ/2/2≅ℤ/2 : AbGroupIso (ℤ/2 /^ 2) ℤ/2
+Iso.fun (fst ℤ/2/2≅ℤ/2) =
+  SQ.rec isSetFin (λ x → x) lem
+  where
+  lem : _
+  lem = ℤ/2-elim (ℤ/2-elim (λ _ → refl)
+        (PT.rec (isSetFin  _ _)
+          (uncurry (ℤ/2-elim
+          (λ p → ⊥.rec (snotz (sym (cong fst p))))
+           λ p → ⊥.rec (snotz (sym (cong fst p)))))))
+        (ℤ/2-elim (PT.rec (isSetFin  _ _)
+          (uncurry (ℤ/2-elim
+          (λ p → ⊥.rec (snotz (sym (cong fst p))))
+           λ p → ⊥.rec (snotz (sym (cong fst p))))))
+          λ _ → refl)
+Iso.inv (fst ℤ/2/2≅ℤ/2) = [_]
+Iso.rightInv (fst ℤ/2/2≅ℤ/2) _ = refl
+Iso.leftInv (fst ℤ/2/2≅ℤ/2) =
+  SQ.elimProp (λ _ → squash/ _ _) λ _ → refl
+snd ℤ/2/2≅ℤ/2 = makeIsGroupHom
+  (SQ.elimProp (λ _ → isPropΠ λ _ → isSetFin _ _)
+  λ a → SQ.elimProp (λ _ → isSetFin _ _) λ b → refl)
+
+ℤTorsion : (n : ℕ) → isContr (fst (ℤAbGroup [ (suc n) ]ₜ))
+fst (ℤTorsion n) = AbGroupStr.0g (snd (ℤAbGroup [ (suc n) ]ₜ))
+snd (ℤTorsion n) (a , p) = Σ≡Prop (λ _ → isSetℤ _ _)
+  (sym (help a (ℤ·≡· (pos (suc n)) a ∙ p)))
+  where
+  help : (a : ℤ) → a +ℤ pos n ·ℤ a ≡ 0 → a ≡ 0
+  help (pos zero) p = refl
+  help (pos (suc a)) p =
+    ⊥.rec (snotz (injPos (pos+ (suc a) (n ·ℕ suc a)
+                 ∙ cong (pos (suc a) +ℤ_) (pos·pos n (suc a)) ∙ p)))
+  help (negsuc a) p = ⊥.rec
+    (snotz (injPos (cong -ℤ_ (negsuc+ a (n ·ℕ suc a)
+                 ∙ (cong (negsuc a +ℤ_)
+                     (cong (-ℤ_) (pos·pos n (suc a)))
+                 ∙ sym (cong (negsuc a +ℤ_) (pos·negsuc n a)) ∙ p)))))

Cubical/Algebra/AbGroup/Instances/Pi.agda

@@ -0,0 +1,12 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.AbGroup.Instances.Pi where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Algebra.AbGroup
+open import Cubical.Algebra.Group.Instances.Pi
+
+module _ {ℓ ℓ' : Level} {X : Type ℓ} (G : X → AbGroup ℓ') where
+  ΠAbGroup : AbGroup (ℓ-max ℓ ℓ')
+  ΠAbGroup = Group→AbGroup (ΠGroup (λ x → AbGroup→Group (G x)))
+              λ f g i x → IsAbGroup.+Comm (AbGroupStr.isAbGroup (G x .snd)) (f x) (g x) i

Cubical/Algebra/AbGroup/Properties.agda

@@ -5,6 +5,17 @@ open import Cubical.Foundations.Prelude
 
 open import Cubical.Algebra.AbGroup.Base
 open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.QuotientGroup
+open import Cubical.Algebra.Group.Subgroup
+open import Cubical.Algebra.Group.ZAction
+
+open import Cubical.HITs.SetQuotients as SQ hiding (_/_)
+
+open import Cubical.Data.Int using (ℤ ; pos ; negsuc)
+open import Cubical.Data.Nat hiding (_+_)
+open import Cubical.Data.Sigma
 
 private variable
   ℓ : Level
@@ -24,3 +35,86 @@ module AbGroupTheory (A : AbGroup ℓ) where
 
   implicitInverse : ∀ {a b} → a + b ≡ 0g → b ≡ - a
   implicitInverse b+a≡0 = invUniqueR b+a≡0
+
+addGroupHom : (A B : AbGroup ℓ) (ϕ ψ : AbGroupHom A B) → AbGroupHom A B
+fst (addGroupHom A B ϕ ψ) x = AbGroupStr._+_ (snd B) (ϕ .fst x) (ψ .fst x)
+snd (addGroupHom A B ϕ ψ) = makeIsGroupHom
+  λ x y → cong₂ (AbGroupStr._+_ (snd B))
+                 (IsGroupHom.pres· (snd ϕ) x y)
+                 (IsGroupHom.pres· (snd ψ) x y)
+        ∙ AbGroupTheory.comm-4 B (fst ϕ x) (fst ϕ y) (fst ψ x) (fst ψ y)
+
+negGroupHom : (A B : AbGroup ℓ) (ϕ : AbGroupHom A B) → AbGroupHom A B
+fst (negGroupHom A B ϕ) x = AbGroupStr.-_ (snd B) (ϕ .fst x)
+snd (negGroupHom A B ϕ) =
+  makeIsGroupHom λ x y
+    → sym (IsGroupHom.presinv (snd ϕ) (AbGroupStr._+_ (snd A) x y))
+     ∙ cong (fst ϕ) (GroupTheory.invDistr (AbGroup→Group A) x y
+                  ∙ AbGroupStr.+Comm (snd A) _ _)
+     ∙ IsGroupHom.pres· (snd ϕ) _ _
+     ∙ cong₂ (AbGroupStr._+_ (snd B))
+             (IsGroupHom.presinv (snd ϕ) x)
+             (IsGroupHom.presinv (snd ϕ) y)
+
+subtrGroupHom : (A B : AbGroup ℓ) (ϕ ψ : AbGroupHom A B) → AbGroupHom A B
+subtrGroupHom A B ϕ ψ = addGroupHom A B ϕ (negGroupHom A B ψ)
+
+
+
+-- ℤ-multiplication defines a homomorphism for abelian groups
+private module _ (G : AbGroup ℓ) where
+  ℤ·isHom-pos : (n : ℕ) (x y : fst G)
+    → (pos n ℤ[ (AbGroup→Group G) ]· (AbGroupStr._+_ (snd G) x y))
+     ≡ AbGroupStr._+_ (snd G) ((pos n) ℤ[ (AbGroup→Group G) ]· x)
+                              ((pos n) ℤ[ (AbGroup→Group G) ]· y)
+  ℤ·isHom-pos zero x y =
+    sym (AbGroupStr.+IdR (snd G) (AbGroupStr.0g (snd G)))
+  ℤ·isHom-pos (suc n) x y =
+    cong₂ (AbGroupStr._+_ (snd G))
+          refl
+          (ℤ·isHom-pos n x y)
+    ∙ AbGroupTheory.comm-4 G _ _ _ _
+
+  ℤ·isHom-neg : (n : ℕ) (x y : fst G)
+    → (negsuc n ℤ[ (AbGroup→Group G) ]· (AbGroupStr._+_ (snd G) x y))
+     ≡ AbGroupStr._+_ (snd G) ((negsuc n) ℤ[ (AbGroup→Group G) ]· x)
+                              ((negsuc n) ℤ[ (AbGroup→Group G) ]· y)
+  ℤ·isHom-neg zero x y =
+    GroupTheory.invDistr (AbGroup→Group G) _ _
+    ∙ AbGroupStr.+Comm (snd G) _ _
+  ℤ·isHom-neg (suc n) x y =
+    cong₂ (AbGroupStr._+_ (snd G))
+          (GroupTheory.invDistr (AbGroup→Group G) _ _
+            ∙ AbGroupStr.+Comm (snd G) _ _)
+          (ℤ·isHom-neg n x y)
+    ∙ AbGroupTheory.comm-4 G _ _ _ _
+
+ℤ·isHom : (n : ℤ) (G : AbGroup ℓ) (x y : fst G)
+  → (n ℤ[ (AbGroup→Group G) ]· (AbGroupStr._+_ (snd G) x y))
+   ≡ AbGroupStr._+_ (snd G) (n ℤ[ (AbGroup→Group G) ]· x)
+                            (n ℤ[ (AbGroup→Group G) ]· y)
+ℤ·isHom (pos n) G = ℤ·isHom-pos G n
+ℤ·isHom (negsuc n) G = ℤ·isHom-neg G n
+
+-- left multiplication as a group homomorphism
+multₗHom : (G : AbGroup ℓ) (n : ℤ) → AbGroupHom G G
+fst (multₗHom G n) g = n ℤ[ (AbGroup→Group G) ]· g
+snd (multₗHom G n) = makeIsGroupHom (ℤ·isHom n G)
+
+-- Abelian groups quotiented by a natural number
+_/^_ : (G : AbGroup ℓ) (n : ℕ) → AbGroup ℓ
+G /^ n =
+  Group→AbGroup
+    ((AbGroup→Group G)
+     / (imSubgroup (multₗHom G (pos n))
+      , isNormalIm (multₗHom G (pos n)) (AbGroupStr.+Comm (snd G))))
+   (SQ.elimProp2 (λ _ _ → squash/ _ _)
+     λ a b → cong [_] (AbGroupStr.+Comm (snd G) a b))
+
+-- Torsion subgrous
+_[_]ₜ : (G : AbGroup ℓ) (n : ℕ) → AbGroup ℓ
+G [ n ]ₜ =
+  Group→AbGroup (Subgroup→Group (AbGroup→Group G)
+    (kerSubgroup (multₗHom G (pos n))))
+    λ {(x , p) (y , q) → Σ≡Prop (λ _ → isPropIsInKer (multₗHom G (pos n)) _)
+      (AbGroupStr.+Comm (snd G) _ _)}

Cubical/Algebra/Group/Instances/IntMod.agda

@@ -4,6 +4,9 @@ module Cubical.Algebra.Group.Instances.IntMod where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Equiv
+
+open import Cubical.Relation.Nullary
 
 open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Unit
@@ -215,3 +218,55 @@ isHomℤ→Fin n =
 
 -Const-ℤ/2 : (x : fst (ℤGroup/ 2)) → -ₘ x ≡ x
 -Const-ℤ/2 = ℤ/2-elim refl refl
+
+pres0→GroupIsoℤ/2 : ∀ {ℓ} {G : Group ℓ} (f : fst G ≃ (ℤGroup/ 2) .fst)
+  → fst f (GroupStr.1g (snd G)) ≡ fzero
+  → IsGroupHom (snd G) (fst f) ((ℤGroup/ 2) .snd)
+pres0→GroupIsoℤ/2 {G = G} f fp = isGroupHomInv ((invEquiv f) , main)
+  where
+  one = invEq f fone
+
+  f⁻∙ : invEq f fzero ≡ GroupStr.1g (snd G)
+  f⁻∙ = sym (cong (invEq f) fp) ∙ retEq f _
+
+  f⁻1 : GroupStr._·_ (snd G) (invEq f fone) (invEq f fone)
+      ≡ GroupStr.1g (snd G)
+  f⁻1 = sym (retEq f (GroupStr._·_ (snd G) (invEq f fone) (invEq f fone)))
+    ∙∙ cong (invEq f) (mainlem _ refl ∙ sym fp)
+    ∙∙ retEq f (GroupStr.1g (snd G))
+    where
+    l : ¬ (fst f (GroupStr._·_ (snd G) (invEq f fone) (invEq f fone))
+                ≡ fone)
+    l p = snotz (cong fst q)
+      where
+      q : fone ≡ fzero
+      q = (sym (secEq f fone)
+        ∙ cong (fst f)
+            ((sym (GroupStr.·IdL (snd G) one)
+            ∙ cong (λ x → GroupStr._·_ (snd G) x one) (sym (GroupStr.·InvL (snd G) one)))
+            ∙ sym (GroupStr.·Assoc (snd G) (GroupStr.inv (snd G) one) one one)))
+        ∙ cong (fst f) (cong (GroupStr._·_ (snd G) (GroupStr.inv (snd G) (invEq f fone)))
+                ((sym (retEq f _) ∙ cong (invEq f) p)))
+        ∙ cong (fst f) (GroupStr.·InvL (snd G) _)
+        ∙ fp
+
+
+    mainlem : (x : _)
+      → fst f (GroupStr._·_ (snd G) (invEq f fone) (invEq f fone)) ≡ x
+      → f .fst ((snd G GroupStr.· invEq f fone) (invEq f fone)) ≡ fzero
+    mainlem = ℤ/2-elim
+      (λ p → p)
+      λ p → ⊥.rec (l p)
+
+
+  main : IsGroupHom ((ℤGroup/ 2) .snd) (invEq f) (snd G)
+  main =
+    makeIsGroupHom
+      (ℤ/2-elim
+        (ℤ/2-elim (f⁻∙ ∙ sym (GroupStr.·IdR (snd G) (GroupStr.1g (snd G)))
+                       ∙ cong (λ x → snd G .GroupStr._·_ x x) (sym f⁻∙))
+                  (sym (GroupStr.·IdL (snd G) one)
+                  ∙ cong (λ x → snd G .GroupStr._·_ x one) (sym f⁻∙)))
+        (ℤ/2-elim (sym (GroupStr.·IdR (snd G) one)
+                  ∙ cong (snd G .GroupStr._·_ (invEq f fone)) (sym f⁻∙))
+                  (f⁻∙ ∙ sym f⁻1)))

Cubical/Algebra/Group/Instances/Pi.agda

@@ -0,0 +1,32 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.Group.Instances.Pi where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Semigroup
+open import Cubical.Algebra.Monoid
+
+open IsGroup
+open GroupStr
+open IsMonoid
+open IsSemigroup
+
+module _ {ℓ ℓ' : Level} {X : Type ℓ} (G : X → Group ℓ') where
+  ΠGroup : Group (ℓ-max ℓ ℓ')
+  fst ΠGroup = (x : X) → fst (G x)
+  1g (snd ΠGroup) x = 1g (G x .snd)
+  GroupStr._·_ (snd ΠGroup) f g x = GroupStr._·_ (G x .snd) (f x) (g x)
+  inv (snd ΠGroup) f x = inv (G x .snd) (f x)
+  is-set (isSemigroup (isMonoid (isGroup (snd ΠGroup)))) =
+    isSetΠ λ x → is-set (G x .snd)
+  IsSemigroup.·Assoc (isSemigroup (isMonoid (isGroup (snd ΠGroup)))) f g h =
+    funExt λ x → IsSemigroup.·Assoc (isSemigroup (isMonoid (G x .snd))) (f x) (g x) (h x)
+  IsMonoid.·IdR (isMonoid (isGroup (snd ΠGroup))) f =
+    funExt λ x → IsMonoid.·IdR (isMonoid (isGroup (snd (G x)))) (f x)
+  IsMonoid.·IdL (isMonoid (isGroup (snd ΠGroup))) f =
+    funExt λ x → IsMonoid.·IdL (isMonoid (isGroup (snd (G x)))) (f x)
+  ·InvR (isGroup (snd ΠGroup)) f =
+    funExt λ x → ·InvR (isGroup (snd (G x))) (f x)
+  ·InvL (isGroup (snd ΠGroup)) f =
+    funExt λ x → ·InvL (isGroup (snd (G x))) (f x)

Cubical/Algebra/Group/MorphismProperties.agda

@@ -177,6 +177,10 @@ compGroupHom : GroupHom F G → GroupHom G H → GroupHom F H
 fst (compGroupHom f g) = fst g ∘ fst f
 snd (compGroupHom f g) = isGroupHomComp f g
 
+trivGroupHom : GroupHom G H
+fst (trivGroupHom {H = H}) _ = 1g (snd H)
+snd (trivGroupHom {H = H}) = makeIsGroupHom λ _ _ → sym (·IdR (snd H) _)
+
 GroupHomDirProd : {A : Group ℓ} {B : Group ℓ'} {C : Group ℓ''} {D : Group ℓ'''}
                 → GroupHom A C → GroupHom B D → GroupHom (DirProd A B) (DirProd C D)
 fst (GroupHomDirProd mf1 mf2) = map-× (fst mf1) (fst mf2)