Skip to content

Commit 573426b

Browse files
aljungstromaljungstrom
authored
Summary file/missing cohomology lemmas (#1092)
* fix * stuff * stuff * more * .. * done? * wups * wups * wups * fixes * ugh...
1 parent e9cf5c6 commit 573426b

40 files changed

+3542
-268
lines changed

‎Cubical/Algebra/AbGroup/Base.agda

-4
Original file line numberDiff line numberDiff line change
@@ -315,10 +315,6 @@ module _ {ℓ ℓ' : Level} (AGr : Group ℓ) (BGr : AbGroup ℓ') where
315315
renaming (_·_ to _∙A_ ; inv to -A_
316316
; 1g to 1A ; ·IdR to ·IdRA)
317317

318-
trivGroupHom : GroupHom AGr (BGr *)
319-
fst trivGroupHom x = 0B
320-
snd trivGroupHom = makeIsGroupHom λ _ _ → sym (+IdRB 0B)
321-
322318
compHom : GroupHom AGr (BGr *) → GroupHom AGr (BGr *) → GroupHom AGr (BGr *)
323319
fst (compHom f g) x = fst f x +B fst g x
324320
snd (compHom f g) =

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

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
{-# OPTIONS --safe #-}
2+
module Cubical.Algebra.AbGroup.Instances.DirectProduct where
3+
4+
open import Cubical.Data.Sigma
5+
open import Cubical.Algebra.AbGroup.Base
6+
open import Cubical.Algebra.Group.DirProd
7+
8+
AbDirProd : ∀ {ℓ ℓ'} → AbGroup ℓ → AbGroup ℓ' → AbGroup (ℓ-max ℓ ℓ')
9+
AbDirProd G H =
10+
Group→AbGroup (DirProd (AbGroup→Group G) (AbGroup→Group H)) comm
11+
where
12+
comm : (x y : fst G × fst H) → _ ≡ _
13+
comm (g1 , h1) (g2 , h2) =
14+
ΣPathP (AbGroupStr.+Comm (snd G) g1 g2
15+
, AbGroupStr.+Comm (snd H) h1 h2)

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

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
{-# OPTIONS --safe #-}
2+
module Cubical.Algebra.AbGroup.Instances.Int where
3+
4+
open import Cubical.Foundations.Prelude
5+
open import Cubical.Data.Int
6+
open import Cubical.Algebra.AbGroup.Base
7+
open import Cubical.Algebra.Group.Base
8+
open import Cubical.Algebra.Group.Instances.Int
9+
10+
ℤAbGroup : AbGroup ℓ-zero
11+
ℤAbGroup = Group→AbGroup ℤGroup +Comm

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

+89
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
{-# OPTIONS --safe #-}
2+
module Cubical.Algebra.AbGroup.Instances.IntMod where
3+
4+
open import Cubical.Foundations.Prelude
5+
open import Cubical.Foundations.Isomorphism
6+
open import Cubical.Foundations.HLevels
7+
open import Cubical.Foundations.Function
8+
9+
open import Cubical.Algebra.AbGroup
10+
11+
open import Cubical.Algebra.Group.Instances.Int
12+
open import Cubical.Algebra.AbGroup.Instances.Int
13+
open import Cubical.Algebra.Group.Instances.IntMod
14+
open import Cubical.Algebra.Group.Base
15+
open import Cubical.Algebra.Group.MorphismProperties
16+
open import Cubical.Algebra.Group.ZAction
17+
18+
open import Cubical.Data.Empty as ⊥
19+
open import Cubical.Data.Nat renaming (_+_ to _+ℕ_ ; _·_ to _·ℕ_)
20+
open import Cubical.Data.Nat.Order
21+
open import Cubical.Data.Int
22+
renaming (_+_ to _+ℤ_ ; _·_ to _·ℤ_ ; -_ to -ℤ_)
23+
open import Cubical.Data.Fin
24+
open import Cubical.Data.Fin.Arithmetic
25+
open import Cubical.Data.Sigma
26+
27+
open import Cubical.HITs.SetQuotients as SQ
28+
open import Cubical.HITs.PropositionalTruncation as PT
29+
30+
ℤAbGroup/_ : ℕ → AbGroup ℓ-zero
31+
ℤAbGroup/ n = Group→AbGroup (ℤGroup/ n) (comm n)
32+
where
33+
comm : (n : ℕ) (x y : fst (ℤGroup/ n))
34+
→ GroupStr._·_ (snd (ℤGroup/ n)) x y
35+
≡ GroupStr._·_ (snd (ℤGroup/ n)) y x
36+
comm zero = +Comm
37+
comm (suc n) = +ₘ-comm
38+
39+
ℤ/2 : AbGroup ℓ-zero
40+
ℤ/2 = ℤAbGroup/ 2
41+
42+
ℤ/2[2]≅ℤ/2 : AbGroupIso (ℤ/2 [ 2 ]ₜ) ℤ/2
43+
Iso.fun (fst ℤ/2[2]≅ℤ/2) = fst
44+
Iso.inv (fst ℤ/2[2]≅ℤ/2) x = x , cong (x +ₘ_) (+ₘ-rUnit x) ∙ x+x x
45+
where
46+
x+x : (x : ℤ/2 .fst) → x +ₘ x ≡ fzero
47+
x+x = ℤ/2-elim refl refl
48+
Iso.rightInv (fst ℤ/2[2]≅ℤ/2) x = Σ≡Prop (λ _ → isProp≤) refl
49+
Iso.leftInv (fst ℤ/2[2]≅ℤ/2) x = Σ≡Prop (λ _ → isSetFin _ _) refl
50+
snd ℤ/2[2]≅ℤ/2 = makeIsGroupHom λ _ _ → refl
51+
52+
ℤ/2/2≅ℤ/2 : AbGroupIso (ℤ/2 /^ 2) ℤ/2
53+
Iso.fun (fst ℤ/2/2≅ℤ/2) =
54+
SQ.rec isSetFin (λ x → x) lem
55+
where
56+
lem : _
57+
lem = ℤ/2-elim (ℤ/2-elim (λ _ → refl)
58+
(PT.rec (isSetFin _ _)
59+
(uncurry (ℤ/2-elim
60+
(λ p → ⊥.rec (snotz (sym (cong fst p))))
61+
λ p → ⊥.rec (snotz (sym (cong fst p)))))))
62+
(ℤ/2-elim (PT.rec (isSetFin _ _)
63+
(uncurry (ℤ/2-elim
64+
(λ p → ⊥.rec (snotz (sym (cong fst p))))
65+
λ p → ⊥.rec (snotz (sym (cong fst p))))))
66+
λ _ → refl)
67+
Iso.inv (fst ℤ/2/2≅ℤ/2) = [_]
68+
Iso.rightInv (fst ℤ/2/2≅ℤ/2) _ = refl
69+
Iso.leftInv (fst ℤ/2/2≅ℤ/2) =
70+
SQ.elimProp (λ _ → squash/ _ _) λ _ → refl
71+
snd ℤ/2/2≅ℤ/2 = makeIsGroupHom
72+
(SQ.elimProp (λ _ → isPropΠ λ _ → isSetFin _ _)
73+
λ a → SQ.elimProp (λ _ → isSetFin _ _) λ b → refl)
74+
75+
ℤTorsion : (n : ℕ) → isContr (fst (ℤAbGroup [ (suc n) ]ₜ))
76+
fst (ℤTorsion n) = AbGroupStr.0g (snd (ℤAbGroup [ (suc n) ]ₜ))
77+
snd (ℤTorsion n) (a , p) = Σ≡Prop (λ _ → isSetℤ _ _)
78+
(sym (help a (ℤ·≡· (pos (suc n)) a ∙ p)))
79+
where
80+
help : (a : ℤ) → a +ℤ pos n ·ℤ a ≡ 0 → a ≡ 0
81+
help (pos zero) p = refl
82+
help (pos (suc a)) p =
83+
⊥.rec (snotz (injPos (pos+ (suc a) (n ·ℕ suc a)
84+
∙ cong (pos (suc a) +ℤ_) (pos·pos n (suc a)) ∙ p)))
85+
help (negsuc a) p = ⊥.rec
86+
(snotz (injPos (cong -ℤ_ (negsuc+ a (n ·ℕ suc a)
87+
∙ (cong (negsuc a +ℤ_)
88+
(cong (-ℤ_) (pos·pos n (suc a)))
89+
∙ sym (cong (negsuc a +ℤ_) (pos·negsuc n a)) ∙ p)))))

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

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
{-# OPTIONS --safe #-}
2+
module Cubical.Algebra.AbGroup.Instances.Pi where
3+
4+
open import Cubical.Foundations.Prelude
5+
open import Cubical.Foundations.HLevels
6+
open import Cubical.Algebra.AbGroup
7+
open import Cubical.Algebra.Group.Instances.Pi
8+
9+
module _ {ℓ ℓ' : Level} {X : Type ℓ} (G : X → AbGroup ℓ') where
10+
ΠAbGroup : AbGroup (ℓ-max ℓ ℓ')
11+
ΠAbGroup = Group→AbGroup (ΠGroup (λ x → AbGroup→Group (G x)))
12+
λ f g i x → IsAbGroup.+Comm (AbGroupStr.isAbGroup (G x .snd)) (f x) (g x) i

‎Cubical/Algebra/AbGroup/Properties.agda

+94
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,17 @@ open import Cubical.Foundations.Prelude
55

66
open import Cubical.Algebra.AbGroup.Base
77
open import Cubical.Algebra.Group
8+
open import Cubical.Algebra.Group.Morphisms
9+
open import Cubical.Algebra.Group.MorphismProperties
10+
open import Cubical.Algebra.Group.QuotientGroup
11+
open import Cubical.Algebra.Group.Subgroup
12+
open import Cubical.Algebra.Group.ZAction
13+
14+
open import Cubical.HITs.SetQuotients as SQ hiding (_/_)
15+
16+
open import Cubical.Data.Int using (ℤ ; pos ; negsuc)
17+
open import Cubical.Data.Nat hiding (_+_)
18+
open import Cubical.Data.Sigma
819

920
private variable
1021
ℓ : Level
@@ -24,3 +35,86 @@ module AbGroupTheory (A : AbGroup ℓ) where
2435

2536
implicitInverse : ∀ {a b} → a + b ≡ 0g → b ≡ - a
2637
implicitInverse b+a≡0 = invUniqueR b+a≡0
38+
39+
addGroupHom : (A B : AbGroup ℓ) (ϕ ψ : AbGroupHom A B) → AbGroupHom A B
40+
fst (addGroupHom A B ϕ ψ) x = AbGroupStr._+_ (snd B) (ϕ .fst x) (ψ .fst x)
41+
snd (addGroupHom A B ϕ ψ) = makeIsGroupHom
42+
λ x y → cong₂ (AbGroupStr._+_ (snd B))
43+
(IsGroupHom.pres· (snd ϕ) x y)
44+
(IsGroupHom.pres· (snd ψ) x y)
45+
∙ AbGroupTheory.comm-4 B (fst ϕ x) (fst ϕ y) (fst ψ x) (fst ψ y)
46+
47+
negGroupHom : (A B : AbGroup ℓ) (ϕ : AbGroupHom A B) → AbGroupHom A B
48+
fst (negGroupHom A B ϕ) x = AbGroupStr.-_ (snd B) (ϕ .fst x)
49+
snd (negGroupHom A B ϕ) =
50+
makeIsGroupHom λ x y
51+
→ sym (IsGroupHom.presinv (snd ϕ) (AbGroupStr._+_ (snd A) x y))
52+
∙ cong (fst ϕ) (GroupTheory.invDistr (AbGroup→Group A) x y
53+
∙ AbGroupStr.+Comm (snd A) _ _)
54+
∙ IsGroupHom.pres· (snd ϕ) _ _
55+
∙ cong₂ (AbGroupStr._+_ (snd B))
56+
(IsGroupHom.presinv (snd ϕ) x)
57+
(IsGroupHom.presinv (snd ϕ) y)
58+
59+
subtrGroupHom : (A B : AbGroup ℓ) (ϕ ψ : AbGroupHom A B) → AbGroupHom A B
60+
subtrGroupHom A B ϕ ψ = addGroupHom A B ϕ (negGroupHom A B ψ)
61+
62+
63+
64+
-- ℤ-multiplication defines a homomorphism for abelian groups
65+
private module _ (G : AbGroup ℓ) where
66+
ℤ·isHom-pos : (n : ℕ) (x y : fst G)
67+
→ (pos n ℤ[ (AbGroup→Group G) ]· (AbGroupStr._+_ (snd G) x y))
68+
≡ AbGroupStr._+_ (snd G) ((pos n) ℤ[ (AbGroup→Group G) ]· x)
69+
((pos n) ℤ[ (AbGroup→Group G) ]· y)
70+
ℤ·isHom-pos zero x y =
71+
sym (AbGroupStr.+IdR (snd G) (AbGroupStr.0g (snd G)))
72+
ℤ·isHom-pos (suc n) x y =
73+
cong₂ (AbGroupStr._+_ (snd G))
74+
refl
75+
(ℤ·isHom-pos n x y)
76+
∙ AbGroupTheory.comm-4 G _ _ _ _
77+
78+
ℤ·isHom-neg : (n : ℕ) (x y : fst G)
79+
→ (negsuc n ℤ[ (AbGroup→Group G) ]· (AbGroupStr._+_ (snd G) x y))
80+
≡ AbGroupStr._+_ (snd G) ((negsuc n) ℤ[ (AbGroup→Group G) ]· x)
81+
((negsuc n) ℤ[ (AbGroup→Group G) ]· y)
82+
ℤ·isHom-neg zero x y =
83+
GroupTheory.invDistr (AbGroup→Group G) _ _
84+
∙ AbGroupStr.+Comm (snd G) _ _
85+
ℤ·isHom-neg (suc n) x y =
86+
cong₂ (AbGroupStr._+_ (snd G))
87+
(GroupTheory.invDistr (AbGroup→Group G) _ _
88+
∙ AbGroupStr.+Comm (snd G) _ _)
89+
(ℤ·isHom-neg n x y)
90+
∙ AbGroupTheory.comm-4 G _ _ _ _
91+
92+
ℤ·isHom : (n : ℤ) (G : AbGroup ℓ) (x y : fst G)
93+
→ (n ℤ[ (AbGroup→Group G) ]· (AbGroupStr._+_ (snd G) x y))
94+
≡ AbGroupStr._+_ (snd G) (n ℤ[ (AbGroup→Group G) ]· x)
95+
(n ℤ[ (AbGroup→Group G) ]· y)
96+
ℤ·isHom (pos n) G = ℤ·isHom-pos G n
97+
ℤ·isHom (negsuc n) G = ℤ·isHom-neg G n
98+
99+
-- left multiplication as a group homomorphism
100+
multₗHom : (G : AbGroup ℓ) (n : ℤ) → AbGroupHom G G
101+
fst (multₗHom G n) g = n ℤ[ (AbGroup→Group G) ]· g
102+
snd (multₗHom G n) = makeIsGroupHom (ℤ·isHom n G)
103+
104+
-- Abelian groups quotiented by a natural number
105+
_/^_ : (G : AbGroup ℓ) (n : ℕ) → AbGroup ℓ
106+
G /^ n =
107+
Group→AbGroup
108+
((AbGroup→Group G)
109+
/ (imSubgroup (multₗHom G (pos n))
110+
, isNormalIm (multₗHom G (pos n)) (AbGroupStr.+Comm (snd G))))
111+
(SQ.elimProp2 (λ _ _ → squash/ _ _)
112+
λ a b → cong [_] (AbGroupStr.+Comm (snd G) a b))
113+
114+
-- Torsion subgrous
115+
_[_]ₜ : (G : AbGroup ℓ) (n : ℕ) → AbGroup ℓ
116+
G [ n ]ₜ =
117+
Group→AbGroup (Subgroup→Group (AbGroup→Group G)
118+
(kerSubgroup (multₗHom G (pos n))))
119+
λ {(x , p) (y , q) → Σ≡Prop (λ _ → isPropIsInKer (multₗHom G (pos n)) _)
120+
(AbGroupStr.+Comm (snd G) _ _)}

‎Cubical/Algebra/Group/Instances/IntMod.agda

+55
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,9 @@ module Cubical.Algebra.Group.Instances.IntMod where
44
open import Cubical.Foundations.Prelude
55
open import Cubical.Foundations.Isomorphism
66
open import Cubical.Foundations.HLevels
7+
open import Cubical.Foundations.Equiv
8+
9+
open import Cubical.Relation.Nullary
710

811
open import Cubical.Data.Empty as ⊥
912
open import Cubical.Data.Unit
@@ -215,3 +218,55 @@ isHomℤ→Fin n =
215218

216219
-Const-ℤ/2 : (x : fst (ℤGroup/ 2)) → -ₘ x ≡ x
217220
-Const-ℤ/2 = ℤ/2-elim refl refl
221+
222+
pres0→GroupIsoℤ/2 : ∀ {ℓ} {G : Group ℓ} (f : fst G ≃ (ℤGroup/ 2) .fst)
223+
→ fst f (GroupStr.1g (snd G)) ≡ fzero
224+
→ IsGroupHom (snd G) (fst f) ((ℤGroup/ 2) .snd)
225+
pres0→GroupIsoℤ/2 {G = G} f fp = isGroupHomInv ((invEquiv f) , main)
226+
where
227+
one = invEq f fone
228+
229+
f⁻∙ : invEq f fzero ≡ GroupStr.1g (snd G)
230+
f⁻∙ = sym (cong (invEq f) fp) ∙ retEq f _
231+
232+
f⁻1 : GroupStr._·_ (snd G) (invEq f fone) (invEq f fone)
233+
≡ GroupStr.1g (snd G)
234+
f⁻1 = sym (retEq f (GroupStr._·_ (snd G) (invEq f fone) (invEq f fone)))
235+
∙∙ cong (invEq f) (mainlem _ refl ∙ sym fp)
236+
∙∙ retEq f (GroupStr.1g (snd G))
237+
where
238+
l : ¬ (fst f (GroupStr._·_ (snd G) (invEq f fone) (invEq f fone))
239+
≡ fone)
240+
l p = snotz (cong fst q)
241+
where
242+
q : fone ≡ fzero
243+
q = (sym (secEq f fone)
244+
∙ cong (fst f)
245+
((sym (GroupStr.·IdL (snd G) one)
246+
∙ cong (λ x → GroupStr._·_ (snd G) x one) (sym (GroupStr.·InvL (snd G) one)))
247+
∙ sym (GroupStr.·Assoc (snd G) (GroupStr.inv (snd G) one) one one)))
248+
∙ cong (fst f) (cong (GroupStr._·_ (snd G) (GroupStr.inv (snd G) (invEq f fone)))
249+
((sym (retEq f _) ∙ cong (invEq f) p)))
250+
∙ cong (fst f) (GroupStr.·InvL (snd G) _)
251+
∙ fp
252+
253+
254+
mainlem : (x : _)
255+
→ fst f (GroupStr._·_ (snd G) (invEq f fone) (invEq f fone)) ≡ x
256+
→ f .fst ((snd G GroupStr.· invEq f fone) (invEq f fone)) ≡ fzero
257+
mainlem = ℤ/2-elim
258+
(λ p → p)
259+
λ p → ⊥.rec (l p)
260+
261+
262+
main : IsGroupHom ((ℤGroup/ 2) .snd) (invEq f) (snd G)
263+
main =
264+
makeIsGroupHom
265+
(ℤ/2-elim
266+
(ℤ/2-elim (f⁻∙ ∙ sym (GroupStr.·IdR (snd G) (GroupStr.1g (snd G)))
267+
∙ cong (λ x → snd G .GroupStr._·_ x x) (sym f⁻∙))
268+
(sym (GroupStr.·IdL (snd G) one)
269+
∙ cong (λ x → snd G .GroupStr._·_ x one) (sym f⁻∙)))
270+
(ℤ/2-elim (sym (GroupStr.·IdR (snd G) one)
271+
∙ cong (snd G .GroupStr._·_ (invEq f fone)) (sym f⁻∙))
272+
(f⁻∙ ∙ sym f⁻1)))

‎Cubical/Algebra/Group/Instances/Pi.agda

+32
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
{-# OPTIONS --safe #-}
2+
module Cubical.Algebra.Group.Instances.Pi where
3+
4+
open import Cubical.Foundations.Prelude
5+
open import Cubical.Foundations.HLevels
6+
open import Cubical.Algebra.Group.Base
7+
open import Cubical.Algebra.Semigroup
8+
open import Cubical.Algebra.Monoid
9+
10+
open IsGroup
11+
open GroupStr
12+
open IsMonoid
13+
open IsSemigroup
14+
15+
module _ {ℓ ℓ' : Level} {X : Type ℓ} (G : X → Group ℓ') where
16+
ΠGroup : Group (ℓ-max ℓ ℓ')
17+
fst ΠGroup = (x : X) → fst (G x)
18+
1g (snd ΠGroup) x = 1g (G x .snd)
19+
GroupStr._·_ (snd ΠGroup) f g x = GroupStr._·_ (G x .snd) (f x) (g x)
20+
inv (snd ΠGroup) f x = inv (G x .snd) (f x)
21+
is-set (isSemigroup (isMonoid (isGroup (snd ΠGroup)))) =
22+
isSetΠ λ x → is-set (G x .snd)
23+
IsSemigroup.·Assoc (isSemigroup (isMonoid (isGroup (snd ΠGroup)))) f g h =
24+
funExt λ x → IsSemigroup.·Assoc (isSemigroup (isMonoid (G x .snd))) (f x) (g x) (h x)
25+
IsMonoid.·IdR (isMonoid (isGroup (snd ΠGroup))) f =
26+
funExt λ x → IsMonoid.·IdR (isMonoid (isGroup (snd (G x)))) (f x)
27+
IsMonoid.·IdL (isMonoid (isGroup (snd ΠGroup))) f =
28+
funExt λ x → IsMonoid.·IdL (isMonoid (isGroup (snd (G x)))) (f x)
29+
·InvR (isGroup (snd ΠGroup)) f =
30+
funExt λ x → ·InvR (isGroup (snd (G x))) (f x)
31+
·InvL (isGroup (snd ΠGroup)) f =
32+
funExt λ x → ·InvL (isGroup (snd (G x))) (f x)

‎Cubical/Algebra/Group/MorphismProperties.agda

+4
Original file line numberDiff line numberDiff line change
@@ -177,6 +177,10 @@ compGroupHom : GroupHom F G → GroupHom G H → GroupHom F H
177177
fst (compGroupHom f g) = fst g ∘ fst f
178178
snd (compGroupHom f g) = isGroupHomComp f g
179179

180+
trivGroupHom : GroupHom G H
181+
fst (trivGroupHom {H = H}) _ = 1g (snd H)
182+
snd (trivGroupHom {H = H}) = makeIsGroupHom λ _ _ → sym (·IdR (snd H) _)
183+
180184
GroupHomDirProd : {A : Group ℓ} {B : Group ℓ'} {C : Group ℓ''} {D : Group ℓ'''}
181185
→ GroupHom A C → GroupHom B D → GroupHom (DirProd A B) (DirProd C D)
182186
fst (GroupHomDirProd mf1 mf2) = map-× (fst mf1) (fst mf2)

0 commit comments

Comments
 (0)