Skip to content

Commit 3306f5b

Browse files
aljungstromaljungstrom
authored
Hurewicz theorem for CW complexes (#1224)
* first * cont * stuff * fixes * more * stuff * stuff * asd * stuff * asd * stuff * done? * minor * minor * Data -> HITs * safe flags * safe flag * wups * universe levels * universe juggling * wups * fixes * remove private
1 parent a1bd3fc commit 3306f5b

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

62 files changed

+8477
-320
lines changed

‎Cubical/Algebra/AbGroup/FinitePresentation.agda‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
module Cubical.Algebra.AbGroup.FinitePresentation where
2+
3+
open import Cubical.Foundations.Prelude
4+
5+
open import Cubical.Data.Nat
6+
open import Cubical.Data.Int
7+
8+
open import Cubical.HITs.PropositionalTruncation
9+
10+
open import Cubical.Algebra.Group
11+
open import Cubical.Algebra.Group.Morphisms
12+
open import Cubical.Algebra.Group.MorphismProperties
13+
open import Cubical.Algebra.AbGroup
14+
open import Cubical.Algebra.AbGroup.Instances.FreeAbGroup
15+
16+
open import Cubical.Algebra.Group.QuotientGroup
17+
open import Cubical.Algebra.Group.Subgroup
18+
19+
private
20+
variable
21+
ℓ : Level
22+
23+
record FinitePresentation (A : AbGroup ℓ) : Type ℓ where
24+
field
25+
nGens : ℕ
26+
nRels : ℕ
27+
rels : AbGroupHom ℤ[Fin nRels ] ℤ[Fin nGens ]
28+
fpiso : AbGroupIso A (ℤ[Fin nGens ] /Im rels)
29+
30+
isFinitelyPresented : AbGroup ℓ → Type ℓ
31+
isFinitelyPresented G = ∥ FinitePresentation G ∥₁
32+
33+
open FinitePresentation
34+
GrIsoPresFinitePresentation : ∀ {ℓ ℓ'} {A : AbGroup ℓ} {B : AbGroup ℓ'}
35+
→ AbGroupIso A B → FinitePresentation A → FinitePresentation B
36+
nGens (GrIsoPresFinitePresentation abG fpA) = nGens fpA
37+
nRels (GrIsoPresFinitePresentation abG fpA) = nRels fpA
38+
rels (GrIsoPresFinitePresentation abG fpA) = rels fpA
39+
fpiso (GrIsoPresFinitePresentation abG fpA) =
40+
compGroupIso (invGroupIso abG) (fpiso fpA)

‎Cubical/Algebra/AbGroup/Instances/FreeAbGroup.agda‎

Lines changed: 114 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ open import Cubical.Foundations.Prelude
55
open import Cubical.Foundations.Function
66
open import Cubical.Foundations.Isomorphism
77
open import Cubical.Foundations.HLevels
8+
open import Cubical.Foundations.Equiv
89

910
open import Cubical.Data.Sigma
1011
open import Cubical.Data.Nat hiding (_·_) renaming (_+_ to _+ℕ_)
@@ -15,6 +16,8 @@ open import Cubical.Data.Fin.Inductive
1516
open import Cubical.Data.Empty as ⊥
1617

1718
open import Cubical.HITs.FreeAbGroup
19+
open import Cubical.HITs.FreeGroup as FG hiding (rec)
20+
open import Cubical.HITs.SetQuotients as SQ hiding (_/_ ; rec)
1821

1922
open import Cubical.Algebra.AbGroup
2023
open import Cubical.Algebra.AbGroup.Instances.Pi
@@ -23,6 +26,10 @@ open import Cubical.Algebra.AbGroup.Instances.DirectProduct
2326
open import Cubical.Algebra.Group
2427
open import Cubical.Algebra.Group.Morphisms
2528
open import Cubical.Algebra.Group.MorphismProperties
29+
open import Cubical.Algebra.Group.Abelianization.Base
30+
open import Cubical.Algebra.Group.Abelianization.Properties as Abi hiding (rec)
31+
open import Cubical.Algebra.Group.Subgroup
32+
open import Cubical.Algebra.Group.QuotientGroup
2633

2734

2835
private variable
@@ -33,11 +40,66 @@ module _ {A : Type ℓ} where
3340
FAGAbGroup : AbGroup ℓ
3441
FAGAbGroup = makeAbGroup {G = FreeAbGroup A} ε _·_ _⁻¹ trunc assoc identityᵣ invᵣ comm
3542

43+
FAGAbGroup→AbGroupHom : ∀ {ℓ ℓ'} {A : Type ℓ} {G : AbGroup ℓ'}
44+
→ (A → fst G) → AbGroupHom (FAGAbGroup {A = A}) G
45+
fst (FAGAbGroup→AbGroupHom {G = G} f) =
46+
Rec.f (AbGroupStr.is-set (snd G)) f
47+
(AbGroupStr.0g (snd G)) (AbGroupStr._+_ (snd G)) (AbGroupStr.-_ (snd G))
48+
(AbGroupStr.+Assoc (snd G)) (AbGroupStr.+Comm (snd G))
49+
(AbGroupStr.+IdR (snd G)) (AbGroupStr.+InvR (snd G))
50+
snd (FAGAbGroup→AbGroupHom {G = G} f) = makeIsGroupHom λ x y → refl
51+
52+
FAGAbGroupGroupHom≡ : ∀ {ℓ ℓ'} {A : Type ℓ} {G : AbGroup ℓ'}
53+
(f g : AbGroupHom (FAGAbGroup {A = A}) G)
54+
→ (∀ a → (fst f) (⟦ a ⟧) ≡ (fst g) (⟦ a ⟧)) → f ≡ g
55+
FAGAbGroupGroupHom≡ {G = G} f g p =
56+
GroupHom≡ (funExt (ElimProp.f (AbGroupStr.is-set (snd G) _ _)
57+
p (IsGroupHom.pres1 (snd f) ∙ sym (IsGroupHom.pres1 (snd g)))
58+
(λ p q → IsGroupHom.pres· (snd f) _ _
59+
∙ cong₂ (AbGroupStr._+_ (snd G)) p q
60+
∙ sym (IsGroupHom.pres· (snd g) _ _))
61+
λ p → IsGroupHom.presinv (snd f) _
62+
∙ cong (AbGroupStr.-_ (snd G)) p
63+
∙ sym (IsGroupHom.presinv (snd g) _)))
64+
65+
module _ {A : Type ℓ} where
66+
freeGroup→freeAbGroup : GroupHom (freeGroupGroup A)
67+
(AbGroup→Group (FAGAbGroup {A = A}))
68+
freeGroup→freeAbGroup = FG.rec {Group = AbGroup→Group (FAGAbGroup {A = A})} ⟦_⟧
69+
70+
AbelienizeFreeGroup→FreeAbGroup :
71+
AbGroupHom (AbelianizationAbGroup (freeGroupGroup A)) (FAGAbGroup {A = A})
72+
AbelienizeFreeGroup→FreeAbGroup =
73+
fromAbelianization FAGAbGroup freeGroup→freeAbGroup
74+
75+
FreeAbGroup→AbelienizeFreeGroup :
76+
AbGroupHom (FAGAbGroup {A = A}) (AbelianizationAbGroup (freeGroupGroup A))
77+
FreeAbGroup→AbelienizeFreeGroup = FAGAbGroup→AbGroupHom λ a → η (η a)
78+
79+
GroupIso-AbelienizeFreeGroup→FreeAbGroup :
80+
AbGroupIso (AbelianizationAbGroup (freeGroupGroup A)) (FAGAbGroup {A = A})
81+
Iso.fun (fst GroupIso-AbelienizeFreeGroup→FreeAbGroup) =
82+
AbelienizeFreeGroup→FreeAbGroup .fst
83+
Iso.inv (fst GroupIso-AbelienizeFreeGroup→FreeAbGroup) =
84+
FreeAbGroup→AbelienizeFreeGroup .fst
85+
Iso.rightInv (fst GroupIso-AbelienizeFreeGroup→FreeAbGroup) x i =
86+
FAGAbGroupGroupHom≡
87+
(compGroupHom FreeAbGroup→AbelienizeFreeGroup
88+
AbelienizeFreeGroup→FreeAbGroup)
89+
idGroupHom (λ _ → refl) i .fst x
90+
Iso.leftInv (fst GroupIso-AbelienizeFreeGroup→FreeAbGroup) =
91+
Abi.elimProp _ (λ _ → isset _ _)
92+
(funExt⁻ (cong fst (freeGroupHom≡
93+
{f = compGroupHom freeGroup→freeAbGroup FreeAbGroup→AbelienizeFreeGroup}
94+
{g = AbelianizationGroupStructure.ηAsGroupHom (freeGroupGroup A)}
95+
λ _ → refl)))
96+
snd GroupIso-AbelienizeFreeGroup→FreeAbGroup =
97+
AbelienizeFreeGroup→FreeAbGroup .snd
98+
3699
-- Alternative definition of case when A = Fin n
37100
ℤ[Fin_] : (n : ℕ) → AbGroup ℓ-zero
38101
ℤ[Fin n ] = ΠℤAbGroup (Fin n)
39102

40-
41103
-- generator of ℤ[Fin_]
42104
ℤFinGenerator : {n : ℕ} (k : Fin n) → ℤ[Fin n ] .fst
43105
ℤFinGenerator {n = n} k s with (fst k ≟ᵗ fst s)
@@ -398,21 +460,21 @@ snd (ℤFinFunct {n = n} {m} f) =
398460
... | gt _ = refl
399461

400462
-- Homs are equal if they agree on generators
401-
agreeOnℤFinGenerator→≡ : ∀ {n m : ℕ}
402-
→ {ϕ ψ : AbGroupHom (ℤ[Fin n ]) (ℤ[Fin m ])}
463+
agreeOnℤFinGenerator→≡ : ∀ {ℓ} {n : ℕ} {G : Group ℓ}
464+
→ {ϕ ψ : GroupHom (AbGroup→Group (ℤ[Fin n ])) G}
403465
→ ((x : _) → fst ϕ (ℤFinGenerator x) ≡ fst ψ (ℤFinGenerator x))
404466
→ ϕ ≡ ψ
405-
agreeOnℤFinGenerator→≡ {n} {m} {ϕ} {ψ} idr =
467+
agreeOnℤFinGenerator→≡ {G = G} {ϕ} {ψ} w =
406468
Σ≡Prop (λ _ → isPropIsGroupHom _ _)
407469
(funExt
408-
(elimPropℤFin _ _ (λ _ → isOfHLevelPath' 1 (isSetΠ (λ _ → isSetℤ)) _ _)
470+
(elimPropℤFin _ _ (λ _ → isOfHLevelPath' 1 (GroupStr.is-set (snd G)) _ _)
409471
(IsGroupHom.pres1 (snd ϕ) ∙ sym (IsGroupHom.pres1 (snd ψ)))
410-
idr
472+
w
411473
(λ f g p q → IsGroupHom.pres· (snd ϕ) f g
412-
∙∙ (λ i x → p i x + q i x)
474+
∙∙ (λ i → GroupStr._·_ (snd G) (p i) (q i))
413475
∙∙ sym (IsGroupHom.pres· (snd ψ) f g ))
414476
λ f p → IsGroupHom.presinv (snd ϕ) f
415-
∙∙ (λ i x → -ℤ (p i x))
477+
∙∙ cong (GroupStr.inv (G .snd) ) p
416478
∙∙ sym (IsGroupHom.presinv (snd ψ) f)))
417479

418480
--
@@ -460,3 +522,47 @@ snd (sumCoefficients n) = makeIsGroupHom (λ x y → funExt λ _ → sumFinℤHo
460522
ℤFinProduct : (n m : ℕ) → AbGroupIso ℤ[Fin (n +ℕ m) ] (AbDirProd ℤ[Fin n ] ℤ[Fin m ])
461523
fst (ℤFinProduct n m) = ℤFinProductIso n m
462524
snd (ℤFinProduct n m) = makeIsGroupHom (λ x y → refl)
525+
526+
-- lemmas about quotients of Free abelian groups
527+
ℤ[]/-GroupHom≡ : ∀ {ℓ} {n : ℕ} (G : Group ℓ)
528+
{Q : NormalSubgroup (AbGroup→Group ℤ[Fin n ])}
529+
(ϕ ψ : GroupHom (AbGroup→Group (ℤ[Fin n ]) / Q ) G)
530+
→ ((k : _) → fst ϕ [ ℤFinGenerator k ] ≡ fst ψ [ ℤFinGenerator k ])
531+
→ ϕ ≡ ψ
532+
ℤ[]/-GroupHom≡ G ϕ ψ s = Σ≡Prop (λ _ → isPropIsGroupHom _ _)
533+
(funExt (SQ.elimProp (λ _ → GroupStr.is-set (snd G) _ _)
534+
λ x → funExt⁻ (cong fst (agreeOnℤFinGenerator→≡
535+
{ϕ = compGroupHom ([_] , makeIsGroupHom λ f g → refl) ϕ}
536+
{ψ = compGroupHom ([_] , makeIsGroupHom λ f g → refl) ψ}
537+
s)) x))
538+
539+
makeℤ[]/Equiv : ∀ {ℓ ℓ'} {G : Group ℓ} {H : Group ℓ'} {n : ℕ}
540+
{T : NormalSubgroup (AbGroup→Group ℤ[Fin n ])}
541+
(ϕ : GroupEquiv (AbGroup→Group ℤ[Fin n ] / T) G)
542+
(ψ : GroupEquiv (AbGroup→Group ℤ[Fin n ] / T) H)
543+
(m : GroupHom G H)
544+
→ ((k : _) → fst m (fst (fst ϕ) [ ℤFinGenerator k ])
545+
≡ fst (fst ψ) [ ℤFinGenerator k ])
546+
→ isEquiv (fst m)
547+
makeℤ[]/Equiv {n = n} {T = T} ϕ ψ m ind =
548+
subst isEquiv (cong fst lem)
549+
(compEquiv (invEquiv (fst ϕ)) (fst ψ) .snd)
550+
where
551+
ξ : GroupHom (AbGroup→Group ℤ[Fin n ] / T) (AbGroup→Group ℤ[Fin n ] / T)
552+
ξ = compGroupHom (GroupEquiv→GroupHom ϕ)
553+
(compGroupHom m (GroupEquiv→GroupHom (invGroupEquiv ψ)))
554+
555+
ξ≡id : ξ ≡ idGroupHom
556+
ξ≡id = ℤ[]/-GroupHom≡ _ _ _
557+
λ w → cong (invEq (fst ψ)) (ind w)
558+
∙ retEq (fst ψ) [ ℤFinGenerator w ]
559+
560+
lem : compGroupHom (GroupEquiv→GroupHom (invGroupEquiv ϕ))
561+
(GroupEquiv→GroupHom ψ)
562+
≡ m
563+
lem = Σ≡Prop (λ _ → isPropIsGroupHom _ _)
564+
(funExt λ x → (sym (funExt⁻
565+
(cong fst (cong (compGroupHom (GroupEquiv→GroupHom (invGroupEquiv ϕ)))
566+
(cong (λ X → compGroupHom X (GroupEquiv→GroupHom ψ)) ξ≡id))) x))
567+
∙ secEq (fst ψ) _
568+
∙ cong (fst m) (secEq (fst ϕ) x))

‎Cubical/Algebra/AbGroup/Properties.agda‎

Lines changed: 10 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,15 @@ snd (negGroupHom A B ϕ) =
6060
subtrGroupHom : (A : AbGroup ℓ) (B : AbGroup ℓ') (ϕ ψ : AbGroupHom A B) → AbGroupHom A B
6161
subtrGroupHom A B ϕ ψ = addGroupHom A B ϕ (negGroupHom A B ψ)
6262

63+
-- Abelian groups quotiented by image of a map
64+
_/Im_ : {H : Group ℓ} (G : AbGroup ℓ) (ϕ : GroupHom H (AbGroup→Group G)) → AbGroup ℓ
65+
G /Im ϕ =
66+
Group→AbGroup (G /' ϕ)
67+
(elimProp2 (λ _ _ → squash/ _ _) λ a b → cong [_] (AbGroupStr.+Comm (snd G) _ _))
68+
where
69+
_/'_ : {H : Group ℓ} (G : AbGroup ℓ) (ϕ : GroupHom H (AbGroup→Group G)) → Group ℓ
70+
G /' ϕ = AbGroup→Group G
71+
/ (imSubgroup ϕ , isNormalIm ϕ λ _ _ → AbGroupStr.+Comm (snd G) _ _)
6372

6473

6574
-- ℤ-multiplication defines a homomorphism for abelian groups
@@ -104,13 +113,7 @@ snd (multₗHom G n) = makeIsGroupHom (ℤ·isHom n G)
104113

105114
-- Abelian groups quotiented by a natural number
106115
_/^_ : (G : AbGroup ℓ) (n : ℕ) → AbGroup ℓ
107-
G /^ n =
108-
Group→AbGroup
109-
((AbGroup→Group G)
110-
/ (imSubgroup (multₗHom G (pos n))
111-
, isNormalIm (multₗHom G (pos n)) (AbGroupStr.+Comm (snd G))))
112-
(SQ.elimProp2 (λ _ _ → squash/ _ _)
113-
λ a b → cong [_] (AbGroupStr.+Comm (snd G) a b))
116+
G /^ n = G /Im multₗHom G (pos n)
114117

115118
-- Torsion subgrous
116119
_[_]ₜ : (G : AbGroup ℓ) (n : ℕ) → AbGroup ℓ

0 commit comments

Comments
 (0)