Hurewicz theorem for CW complexes

Cubical/Algebra/AbGroup/FinitePresentation.agda

@@ -0,0 +1,40 @@
+module Cubical.Algebra.AbGroup.FinitePresentation where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Data.Nat
+open import Cubical.Data.Int
+
+open import Cubical.HITs.PropositionalTruncation
+
+open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.AbGroup
+open import Cubical.Algebra.AbGroup.Instances.FreeAbGroup
+
+open import Cubical.Algebra.Group.QuotientGroup
+open import Cubical.Algebra.Group.Subgroup
+
+private
+  variable
+    ℓ : Level
+
+record FinitePresentation (A : AbGroup ℓ) : Type ℓ where
+  field
+    nGens : ℕ
+    nRels : ℕ
+    rels : AbGroupHom ℤ[Fin nRels ] ℤ[Fin nGens ]
+    fpiso : AbGroupIso A (ℤ[Fin nGens ] /Im rels)
+
+isFinitelyPresented : AbGroup ℓ → Type ℓ
+isFinitelyPresented G = ∥ FinitePresentation G ∥₁
+
+open FinitePresentation
+GrIsoPresFinitePresentation : ∀ {ℓ ℓ'} {A : AbGroup ℓ} {B : AbGroup ℓ'}
+  → AbGroupIso A B → FinitePresentation A → FinitePresentation B
+nGens (GrIsoPresFinitePresentation abG fpA) = nGens fpA
+nRels (GrIsoPresFinitePresentation abG fpA) = nRels fpA
+rels (GrIsoPresFinitePresentation abG fpA) = rels fpA
+fpiso (GrIsoPresFinitePresentation abG fpA) =
+  compGroupIso (invGroupIso abG) (fpiso fpA)

Cubical/Algebra/AbGroup/Instances/FreeAbGroup.agda

@@ -5,6 +5,7 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Equiv
 
 open import Cubical.Data.Sigma
 open import Cubical.Data.Nat hiding (_·_) renaming (_+_ to _+ℕ_)
@@ -15,6 +16,8 @@ open import Cubical.Data.Fin.Inductive
 open import Cubical.Data.Empty as ⊥
 
 open import Cubical.HITs.FreeAbGroup
+open import Cubical.HITs.FreeGroup as FG hiding (rec)
+open import Cubical.HITs.SetQuotients as SQ hiding (_/_ ; rec)
 
 open import Cubical.Algebra.AbGroup
 open import Cubical.Algebra.AbGroup.Instances.Pi
@@ -23,6 +26,10 @@ open import Cubical.Algebra.AbGroup.Instances.DirectProduct
 open import Cubical.Algebra.Group
 open import Cubical.Algebra.Group.Morphisms
 open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.Abelianization.Base
+open import Cubical.Algebra.Group.Abelianization.Properties as Abi hiding (rec)
+open import Cubical.Algebra.Group.Subgroup
+open import Cubical.Algebra.Group.QuotientGroup
 
 
 private variable
@@ -33,11 +40,66 @@ module _ {A : Type ℓ} where
   FAGAbGroup : AbGroup ℓ
   FAGAbGroup = makeAbGroup {G = FreeAbGroup A} ε _·_ _⁻¹ trunc assoc identityᵣ invᵣ comm
 
+FAGAbGroup→AbGroupHom : ∀ {ℓ ℓ'} {A : Type ℓ} {G : AbGroup ℓ'}
+  → (A → fst G) → AbGroupHom (FAGAbGroup {A = A}) G
+fst (FAGAbGroup→AbGroupHom {G = G} f) =
+  Rec.f (AbGroupStr.is-set (snd G)) f
+    (AbGroupStr.0g (snd G)) (AbGroupStr._+_ (snd G)) (AbGroupStr.-_ (snd G))
+    (AbGroupStr.+Assoc (snd G)) (AbGroupStr.+Comm (snd G))
+    (AbGroupStr.+IdR (snd G)) (AbGroupStr.+InvR (snd G))
+snd (FAGAbGroup→AbGroupHom {G = G} f) = makeIsGroupHom λ x y → refl
+
+FAGAbGroupGroupHom≡ : ∀ {ℓ ℓ'} {A : Type ℓ} {G : AbGroup ℓ'}
+  (f g : AbGroupHom (FAGAbGroup {A = A}) G)
+  → (∀ a → (fst f) (⟦ a ⟧) ≡ (fst g) (⟦ a ⟧)) → f ≡ g
+FAGAbGroupGroupHom≡ {G = G} f g p =
+  GroupHom≡ (funExt (ElimProp.f (AbGroupStr.is-set (snd G) _ _)
+    p (IsGroupHom.pres1 (snd f) ∙ sym (IsGroupHom.pres1 (snd g)))
+    (λ p q → IsGroupHom.pres· (snd f) _ _
+            ∙ cong₂ (AbGroupStr._+_ (snd G)) p q
+            ∙ sym (IsGroupHom.pres· (snd g) _ _))
+    λ p → IsGroupHom.presinv (snd f) _
+        ∙ cong (AbGroupStr.-_ (snd G)) p
+        ∙ sym (IsGroupHom.presinv (snd g) _)))
+
+module _ {A : Type ℓ} where
+  freeGroup→freeAbGroup : GroupHom (freeGroupGroup A)
+                                    (AbGroup→Group (FAGAbGroup {A = A}))
+  freeGroup→freeAbGroup = FG.rec {Group = AbGroup→Group (FAGAbGroup {A = A})} ⟦_⟧
+
+  AbelienizeFreeGroup→FreeAbGroup :
+    AbGroupHom (AbelianizationAbGroup (freeGroupGroup A)) (FAGAbGroup {A = A})
+  AbelienizeFreeGroup→FreeAbGroup =
+    fromAbelianization FAGAbGroup freeGroup→freeAbGroup
+
+  FreeAbGroup→AbelienizeFreeGroup :
+    AbGroupHom (FAGAbGroup {A = A}) (AbelianizationAbGroup (freeGroupGroup A))
+  FreeAbGroup→AbelienizeFreeGroup = FAGAbGroup→AbGroupHom λ a → η (η a)
+
+  GroupIso-AbelienizeFreeGroup→FreeAbGroup :
+    AbGroupIso (AbelianizationAbGroup (freeGroupGroup A)) (FAGAbGroup {A = A})
+  Iso.fun (fst GroupIso-AbelienizeFreeGroup→FreeAbGroup) =
+    AbelienizeFreeGroup→FreeAbGroup .fst
+  Iso.inv (fst GroupIso-AbelienizeFreeGroup→FreeAbGroup) =
+    FreeAbGroup→AbelienizeFreeGroup .fst
+  Iso.rightInv (fst GroupIso-AbelienizeFreeGroup→FreeAbGroup) x i =
+    FAGAbGroupGroupHom≡
+      (compGroupHom FreeAbGroup→AbelienizeFreeGroup
+                    AbelienizeFreeGroup→FreeAbGroup)
+      idGroupHom (λ _ → refl) i .fst x
+  Iso.leftInv (fst GroupIso-AbelienizeFreeGroup→FreeAbGroup) =
+    Abi.elimProp _ (λ _ → isset _ _)
+    (funExt⁻ (cong fst (freeGroupHom≡
+      {f = compGroupHom  freeGroup→freeAbGroup FreeAbGroup→AbelienizeFreeGroup}
+      {g = AbelianizationGroupStructure.ηAsGroupHom (freeGroupGroup A)}
+      λ _ → refl)))
+  snd GroupIso-AbelienizeFreeGroup→FreeAbGroup =
+    AbelienizeFreeGroup→FreeAbGroup .snd
+
 -- Alternative definition of case when A = Fin n
 ℤ[Fin_] : (n : ℕ) → AbGroup ℓ-zero
 ℤ[Fin n ] = ΠℤAbGroup (Fin n)
 
-
 --  generator of ℤ[Fin_]
 ℤFinGenerator : {n : ℕ} (k : Fin n) → ℤ[Fin n ] .fst
 ℤFinGenerator {n = n} k s with (fst k ≟ᵗ fst s)
@@ -398,21 +460,21 @@ snd (ℤFinFunct {n = n} {m} f) =
   ... | gt _ = refl
 
 -- Homs are equal if they agree on generators
-agreeOnℤFinGenerator→≡ : ∀ {n m : ℕ}
-  → {ϕ ψ : AbGroupHom (ℤ[Fin n ]) (ℤ[Fin m ])}
+agreeOnℤFinGenerator→≡ : ∀ {ℓ} {n : ℕ} {G : Group ℓ}
+  → {ϕ ψ : GroupHom (AbGroup→Group (ℤ[Fin n ])) G}
   → ((x : _) → fst ϕ (ℤFinGenerator x) ≡ fst ψ (ℤFinGenerator x))
   → ϕ ≡ ψ
-agreeOnℤFinGenerator→≡ {n} {m} {ϕ} {ψ} idr =
+agreeOnℤFinGenerator→≡ {G = G} {ϕ} {ψ} w =
   Σ≡Prop (λ _ → isPropIsGroupHom _ _)
    (funExt
-    (elimPropℤFin _ _ (λ _ → isOfHLevelPath' 1 (isSetΠ (λ _ → isSetℤ)) _ _)
+    (elimPropℤFin _ _ (λ _ → isOfHLevelPath' 1 (GroupStr.is-set (snd G)) _ _)
       (IsGroupHom.pres1 (snd ϕ) ∙ sym (IsGroupHom.pres1 (snd ψ)))
-      idr
+      w
       (λ f g p q → IsGroupHom.pres· (snd ϕ) f g
-                 ∙∙ (λ i x → p i x + q i x)
+                 ∙∙ (λ i → GroupStr._·_ (snd G) (p i) (q i))
                  ∙∙ sym (IsGroupHom.pres· (snd ψ) f g ))
       λ f p → IsGroupHom.presinv (snd ϕ) f
-           ∙∙ (λ i x → -ℤ (p i x))
+           ∙∙ cong (GroupStr.inv (G .snd) ) p
            ∙∙ sym (IsGroupHom.presinv (snd ψ) f)))
 
 --
@@ -460,3 +522,47 @@ snd (sumCoefficients n) = makeIsGroupHom (λ x y → funExt λ _ → sumFinℤHo
 ℤFinProduct : (n m : ℕ) → AbGroupIso ℤ[Fin (n +ℕ m) ] (AbDirProd ℤ[Fin n ] ℤ[Fin m ])
 fst (ℤFinProduct n m) = ℤFinProductIso n m
 snd (ℤFinProduct n m) = makeIsGroupHom (λ x y → refl)
+
+-- lemmas about quotients of Free abelian groups
+ℤ[]/-GroupHom≡ : ∀ {ℓ} {n : ℕ} (G : Group ℓ)
+  {Q : NormalSubgroup (AbGroup→Group ℤ[Fin n ])}
+  (ϕ ψ : GroupHom (AbGroup→Group (ℤ[Fin n ]) / Q ) G)
+ → ((k : _) → fst ϕ [ ℤFinGenerator k ] ≡ fst ψ [ ℤFinGenerator k ])
+ → ϕ ≡ ψ
+ℤ[]/-GroupHom≡ G ϕ ψ s = Σ≡Prop (λ _ → isPropIsGroupHom _ _)
+  (funExt (SQ.elimProp (λ _ → GroupStr.is-set (snd G) _ _)
+    λ x → funExt⁻ (cong fst (agreeOnℤFinGenerator→≡
+      {ϕ = compGroupHom ([_] , makeIsGroupHom λ f g → refl) ϕ}
+      {ψ = compGroupHom ([_] , makeIsGroupHom λ f g → refl) ψ}
+      s)) x))
+
+makeℤ[]/Equiv : ∀ {ℓ ℓ'} {G : Group ℓ} {H : Group ℓ'} {n : ℕ}
+  {T : NormalSubgroup (AbGroup→Group ℤ[Fin n ])}
+  (ϕ : GroupEquiv (AbGroup→Group ℤ[Fin n ] / T) G)
+  (ψ : GroupEquiv (AbGroup→Group ℤ[Fin n ] / T) H)
+  (m : GroupHom G H)
+  → ((k : _) → fst m (fst (fst ϕ) [ ℤFinGenerator k ])
+              ≡ fst (fst ψ) [ ℤFinGenerator k ])
+  → isEquiv (fst m)
+makeℤ[]/Equiv {n = n} {T = T} ϕ ψ m ind =
+  subst isEquiv (cong fst lem)
+    (compEquiv (invEquiv (fst ϕ)) (fst ψ) .snd)
+  where
+  ξ : GroupHom (AbGroup→Group ℤ[Fin n ] / T) (AbGroup→Group ℤ[Fin n ] / T)
+  ξ = compGroupHom (GroupEquiv→GroupHom ϕ)
+          (compGroupHom m (GroupEquiv→GroupHom (invGroupEquiv ψ)))
+
+  ξ≡id : ξ ≡ idGroupHom
+  ξ≡id = ℤ[]/-GroupHom≡ _ _ _
+    λ w → cong (invEq (fst ψ)) (ind w)
+         ∙ retEq (fst ψ) [ ℤFinGenerator w ]
+
+  lem : compGroupHom (GroupEquiv→GroupHom (invGroupEquiv ϕ))
+                      (GroupEquiv→GroupHom ψ)
+       ≡ m
+  lem = Σ≡Prop (λ _ → isPropIsGroupHom _ _)
+    (funExt λ x → (sym (funExt⁻
+      (cong fst (cong (compGroupHom (GroupEquiv→GroupHom (invGroupEquiv ϕ)))
+             (cong (λ X → compGroupHom X (GroupEquiv→GroupHom ψ)) ξ≡id))) x))
+       ∙ secEq (fst ψ) _
+       ∙ cong (fst m) (secEq (fst ϕ) x))

Cubical/Algebra/AbGroup/Properties.agda

@@ -60,6 +60,15 @@ snd (negGroupHom A B ϕ) =
 subtrGroupHom : (A : AbGroup ℓ) (B : AbGroup ℓ') (ϕ ψ : AbGroupHom A B) → AbGroupHom A B
 subtrGroupHom A B ϕ ψ = addGroupHom A B ϕ (negGroupHom A B ψ)
 
+-- Abelian groups quotiented by image of a map
+_/Im_ : {H : Group ℓ} (G : AbGroup ℓ) (ϕ : GroupHom H (AbGroup→Group G)) → AbGroup ℓ
+G /Im ϕ =
+  Group→AbGroup (G /' ϕ)
+    (elimProp2 (λ _ _ → squash/ _ _) λ a b → cong [_] (AbGroupStr.+Comm (snd G) _ _))
+  where
+  _/'_ : {H : Group ℓ} (G : AbGroup ℓ) (ϕ : GroupHom H (AbGroup→Group G)) → Group ℓ
+  G /' ϕ = AbGroup→Group G
+          / (imSubgroup ϕ , isNormalIm ϕ λ _ _ → AbGroupStr.+Comm (snd G) _ _)
 
 
 -- ℤ-multiplication defines a homomorphism for abelian groups
@@ -104,13 +113,7 @@ 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))
+G /^ n = G /Im multₗHom G (pos n)
 
 -- Torsion subgrous
 _[_]ₜ : (G : AbGroup ℓ) (n : ℕ) → AbGroup ℓ