-
Notifications
You must be signed in to change notification settings - Fork 141
/
MayerVietorisUnreduced.agda
258 lines (225 loc) · 14.3 KB
/
MayerVietorisUnreduced.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
{-# OPTIONS --safe #-}
module Cubical.ZCohomology.MayerVietorisUnreduced where
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Path
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Data.Nat
open import Cubical.Data.Sigma
open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.DirProd
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Instances.Bool
open import Cubical.Algebra.Group.Instances.Int
open import Cubical.Algebra.Group.Instances.Unit
open import Cubical.HITs.SetTruncation as ST
open import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.HITs.Pushout
open import Cubical.HITs.Sn
open import Cubical.HITs.S1
open import Cubical.HITs.Susp
open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.GroupStructure
open IsGroupHom
module MV {ℓ ℓ' ℓ''} (A : Type ℓ) (B : Type ℓ') (C : Type ℓ'') (f : C → A) (g : C → B) where
-- Proof from Brunerie 2016.
-- We first define the three morphisms involved: i, Δ and d.
private
i* : (n : ℕ) → coHom n (Pushout f g) → coHom n A × coHom n B
i* n = ST.rec (isSet× isSetSetTrunc isSetSetTrunc) λ δ → ∣ (λ x → δ (inl x)) ∣₂ , ∣ (λ x → δ (inr x)) ∣₂
iIsHom : (n : ℕ) → IsGroupHom (coHomGr n (Pushout f g) .snd) (i* n) (×coHomGr n A B .snd)
iIsHom n =
makeIsGroupHom (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSet× isSetSetTrunc isSetSetTrunc) _ _) λ _ _ → refl)
i : (n : ℕ) → GroupHom (coHomGr n (Pushout f g)) (×coHomGr n A B)
fst (i n) = i* n
snd (i n) = iIsHom n
private
distrLem : (n : ℕ) (x y z w : coHomK n) → (x +[ n ]ₖ y) -[ n ]ₖ (z +[ n ]ₖ w) ≡ (x -[ n ]ₖ z) +[ n ]ₖ (y -[ n ]ₖ w)
distrLem n x y z w = cong (λ z → (x +[ n ]ₖ y) +[ n ]ₖ z) (-distrₖ n z w)
∙∙ sym (assocₖ n x y ((-[ n ]ₖ z) +[ n ]ₖ (-[ n ]ₖ w)))
∙∙ cong (λ y → x +[ n ]ₖ y) (commₖ n y ((-[ n ]ₖ z) +[ n ]ₖ (-[ n ]ₖ w)) ∙ sym (assocₖ n _ _ _))
∙∙ assocₖ n _ _ _
∙∙ cong (λ y → (x -[ n ]ₖ z) +[ n ]ₖ y) (commₖ n (-[ n ]ₖ w) y)
Δ' : (n : ℕ) → coHom n A × coHom n B → coHom n C
Δ' n (α , β) = coHomFun n f α -[ n ]ₕ coHomFun n g β
Δ'-isMorph : (n : ℕ) → IsGroupHom (×coHomGr n A B .snd) (Δ' n) (coHomGr n C .snd)
Δ'-isMorph n =
makeIsGroupHom
(prodElim2 (λ _ _ → isOfHLevelPath 2 isSetSetTrunc _ _ )
λ f' x1 g' x2 i → ∣ (λ x → distrLem n (f' (f x)) (g' (f x)) (x1 (g x)) (x2 (g x)) i) ∣₂)
Δ : (n : ℕ) → GroupHom (×coHomGr n A B) (coHomGr n C)
fst (Δ n) = Δ' n
snd (Δ n) = Δ'-isMorph n
d-pre : (n : ℕ) → (C → coHomK n) → Pushout f g → coHomK (suc n)
d-pre n γ (inl x) = 0ₖ (suc n)
d-pre n γ (inr x) = 0ₖ (suc n)
d-pre n γ (push a i) = Kn→ΩKn+1 n (γ a) i
dHomHelper : (n : ℕ) (h l : C → coHomK n) (x : Pushout f g)
→ d-pre n (λ x → h x +[ n ]ₖ l x) x ≡ d-pre n h x +[ suc n ]ₖ d-pre n l x
dHomHelper n h l (inl x) = sym (rUnitₖ (suc n) (0ₖ (suc n)))
dHomHelper n h l (inr x) = sym (lUnitₖ (suc n) (0ₖ (suc n)))
dHomHelper n h l (push a i) j =
hcomp (λ k → λ { (i = i0) → rUnitₖ (suc n) (0ₖ (suc n)) (~ j)
; (i = i1) → lUnitₖ (suc n) (0ₖ (suc n)) (~ j)
; (j = i0) → Kn→ΩKn+1-hom n (h a) (l a) (~ k) i
; (j = i1) → cong₂Funct (λ x y → x +[ (suc n) ]ₖ y) (Kn→ΩKn+1 n (h a)) (Kn→ΩKn+1 n (l a)) (~ k) i })
(hcomp (λ k → λ { (i = i0) → rUnitₖ (suc n) (0ₖ (suc n)) (~ j)
; (i = i1) → lUnitₖ (suc n) (Kn→ΩKn+1 n (l a) k) (~ j)})
(hcomp (λ k → λ { (i = i0) → rUnitₖ (suc n) (0ₖ (suc n)) (~ j)
; (i = i1) → lUnitₖ≡rUnitₖ (suc n) (~ k) (~ j)
; (j = i0) → Kn→ΩKn+1 n (h a) i
; (j = i1) → (Kn→ΩKn+1 n (h a) i) +[ (suc n) ]ₖ coHom-pt (suc n)})
(rUnitₖ (suc n) (Kn→ΩKn+1 n (h a) i) (~ j))))
dIsHom : (n : ℕ) → IsGroupHom (coHomGr n C .snd) (ST.rec isSetSetTrunc λ a → ∣ d-pre n a ∣₂) (coHomGr (suc n) (Pushout f g) .snd)
dIsHom n =
makeIsGroupHom
(ST.elim2 (λ _ _ → isOfHLevelPath 2 isSetSetTrunc _ _)
λ f g i → ∣ funExt (λ x → dHomHelper n f g x) i ∣₂)
d : (n : ℕ) → GroupHom (coHomGr n C) (coHomGr (suc n) (Pushout f g))
fst (d n) = ST.rec isSetSetTrunc λ a → ∣ d-pre n a ∣₂
snd (d n) = dIsHom n
-- The long exact sequence
Im-d⊂Ker-i : (n : ℕ) (x : ⟨ (coHomGr (suc n) (Pushout f g)) ⟩)
→ isInIm (d n) x
→ isInKer (i (suc n)) x
Im-d⊂Ker-i n = ST.elim (λ _ → isSetΠ λ _ → isOfHLevelPath 2 (isSet× isSetSetTrunc isSetSetTrunc) _ _)
λ a → PT.rec (isOfHLevelPath' 1 (isSet× isSetSetTrunc isSetSetTrunc) _ _)
(sigmaElim (λ _ → isOfHLevelPath 2 (isSet× isSetSetTrunc isSetSetTrunc) _ _)
λ δ b i → ST.rec (isSet× isSetSetTrunc isSetSetTrunc)
(λ δ → ∣ (λ x → δ (inl x)) ∣₂ , ∣ (λ x → δ (inr x)) ∣₂ ) (b (~ i)))
Ker-i⊂Im-d : (n : ℕ) (x : ⟨ coHomGr (suc n) (Pushout f g) ⟩)
→ isInKer (i (suc n)) x
→ isInIm (d n) x
Ker-i⊂Im-d n =
ST.elim (λ _ → isSetΠ λ _ → isProp→isSet isPropPropTrunc)
λ a p → PT.rec {A = (λ x → a (inl x)) ≡ λ _ → 0ₖ (suc n)}
(isProp→ isPropPropTrunc)
(λ p1 → PT.rec isPropPropTrunc λ p2 → ∣ ∣ (λ c → ΩKn+1→Kn n (sym (cong (λ F → F (f c)) p1)
∙∙ cong a (push c)
∙∙ cong (λ F → F (g c)) p2)) ∣₂
, cong ∣_∣₂ (funExt (λ δ → helper a p1 p2 δ)) ∣₁)
(Iso.fun PathIdTrunc₀Iso (cong fst p))
(Iso.fun PathIdTrunc₀Iso (cong snd p))
where
helper : (F : (Pushout f g) → coHomK (suc n))
(p1 : Path (_ → coHomK (suc n)) (λ a₁ → F (inl a₁)) (λ _ → coHom-pt (suc n)))
(p2 : Path (_ → coHomK (suc n)) (λ a₁ → F (inr a₁)) (λ _ → coHom-pt (suc n)))
→ (δ : Pushout f g)
→ d-pre n (λ c → ΩKn+1→Kn n ((λ i₁ → p1 (~ i₁) (f c))
∙∙ cong F (push c)
∙∙ cong (λ F → F (g c)) p2)) δ
≡ F δ
helper F p1 p2 (inl x) = sym (cong (λ f → f x) p1)
helper F p1 p2 (inr x) = sym (cong (λ f → f x) p2)
helper F p1 p2 (push a i) j =
hcomp (λ k → λ { (i = i0) → p1 (~ j) (f a)
; (i = i1) → p2 (~ j) (g a)
; (j = i0) → Iso.rightInv (Iso-Kn-ΩKn+1 n) ((λ i₁ → p1 (~ i₁) (f a))
∙∙ cong F (push a)
∙∙ cong (λ F₁ → F₁ (g a)) p2) (~ k) i
; (j = i1) → F (push a i)})
(doubleCompPath-filler (sym (cong (λ F → F (f a)) p1)) (cong F (push a)) (cong (λ F → F (g a)) p2) (~ j) i)
Im-i⊂Ker-Δ : (n : ℕ) (x : ⟨ ×coHomGr n A B ⟩)
→ isInIm (i n) x
→ isInKer (Δ n) x
Im-i⊂Ker-Δ n (Fa , Fb) =
ST.elim {B = λ Fa → (Fb : _) → isInIm (i n) (Fa , Fb)
→ isInKer (Δ n) (Fa , Fb)}
(λ _ → isSetΠ2 λ _ _ → isOfHLevelPath 2 isSetSetTrunc _ _)
(λ Fa → ST.elim (λ _ → isSetΠ λ _ → isOfHLevelPath 2 isSetSetTrunc _ _)
λ Fb → PT.rec (isSetSetTrunc _ _)
(sigmaElim (λ x → isProp→isSet (isSetSetTrunc _ _))
λ Fd p → helper n Fa Fb Fd p))
Fa
Fb
where
helper : (n : ℕ) (Fa : A → coHomK n) (Fb : B → coHomK n) (Fd : (Pushout f g) → coHomK n)
→ (fst (i n) ∣ Fd ∣₂ ≡ (∣ Fa ∣₂ , ∣ Fb ∣₂))
→ (fst (Δ n)) (∣ Fa ∣₂ , ∣ Fb ∣₂) ≡ 0ₕ n
helper n Fa Fb Fd p = cong (fst (Δ n)) (sym p)
∙∙ (λ i → ∣ (λ x → Fd (inl (f x))) ∣₂ -[ n ]ₕ ∣ (λ x → Fd (push x (~ i))) ∣₂ )
∙∙ rCancelₕ n ∣ (λ x → Fd (inl (f x))) ∣₂
Ker-Δ⊂Im-i : (n : ℕ) (a : ⟨ ×coHomGr n A B ⟩)
→ isInKer (Δ n) a
→ isInIm (i n) a
Ker-Δ⊂Im-i n = prodElim (λ _ → isSetΠ (λ _ → isProp→isSet isPropPropTrunc))
(λ Fa Fb p → PT.rec isPropPropTrunc
(λ q → ∣ ∣ helpFun Fa Fb q ∣₂ , refl ∣₁)
(helper Fa Fb p))
where
helper : (Fa : A → coHomK n) (Fb : B → coHomK n)
→ fst (Δ n) (∣ Fa ∣₂ , ∣ Fb ∣₂) ≡ 0ₕ n
→ ∥ Path (_ → _) (λ c → Fa (f c)) (λ c → Fb (g c)) ∥₁
helper Fa Fb p = Iso.fun PathIdTrunc₀Iso
(sym (cong ∣_∣₂ (funExt (λ x → sym (assocₖ n _ _ _)
∙∙ cong (λ y → Fa (f x) +[ n ]ₖ y) (lCancelₖ n (Fb (g x)))
∙∙ rUnitₖ n (Fa (f x)))))
∙∙ cong (λ x → x +[ n ]ₕ ∣ (λ c → Fb (g c)) ∣₂) p
∙∙ lUnitₕ n _)
helpFun : (Fa : A → coHomK n) (Fb : B → coHomK n)
→ ((λ c → Fa (f c)) ≡ (λ c → Fb (g c)))
→ Pushout f g → coHomK n
helpFun Fa Fb p (inl x) = Fa x
helpFun Fa Fb p (inr x) = Fb x
helpFun Fa Fb p (push a i) = p i a
private
distrHelper : (n : ℕ) (p q : _)
→ ΩKn+1→Kn n p +[ n ]ₖ (-[ n ]ₖ ΩKn+1→Kn n q) ≡ ΩKn+1→Kn n (p ∙ sym q)
distrHelper n p q = cong (λ x → ΩKn+1→Kn n p +[ n ]ₖ x) helper ∙ sym (ΩKn+1→Kn-hom n _ _)
where
helper : -[ n ]ₖ ΩKn+1→Kn n q ≡ ΩKn+1→Kn n (sym q)
helper =
sym (rUnitₖ n _)
∙∙ cong (λ x → (-[ n ]ₖ (ΩKn+1→Kn n q)) +[ n ]ₖ x) (sym helper2)
∙∙ (assocₖ n _ _ _ ∙∙ cong (λ x → x +[ n ]ₖ (ΩKn+1→Kn n (sym q))) (lCancelₖ n _) ∙∙ lUnitₖ n _)
where
helper2 : ΩKn+1→Kn n q +[ n ]ₖ (ΩKn+1→Kn n (sym q)) ≡ coHom-pt n
helper2 = sym (ΩKn+1→Kn-hom n q (sym q)) ∙∙ cong (ΩKn+1→Kn n) (rCancel q) ∙∙ ΩKn+1→Kn-refl n
Ker-d⊂Im-Δ : (n : ℕ) (a : coHom n C)
→ isInKer (d n) a
→ isInIm (Δ n) a
Ker-d⊂Im-Δ n =
ST.elim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 isPropPropTrunc)
λ Fc p → PT.rec isPropPropTrunc (λ p → ∣ (∣ (λ a → ΩKn+1→Kn n (cong (λ f → f (inl a)) p)) ∣₂ ,
∣ (λ b → ΩKn+1→Kn n (cong (λ f → f (inr b)) p)) ∣₂) ,
Iso.inv (PathIdTrunc₀Iso) ∣ funExt (λ c → helper2 Fc p c) ∣₁ ∣₁)
(Iso.fun (PathIdTrunc₀Iso) p)
where
helper2 : (Fc : C → coHomK n)
(p : d-pre n Fc ≡ (λ _ → coHom-pt (suc n))) (c : C)
→ ΩKn+1→Kn n (λ i₁ → p i₁ (inl (f c))) -[ n ]ₖ (ΩKn+1→Kn n (λ i₁ → p i₁ (inr (g c)))) ≡ Fc c
helper2 Fc p c = distrHelper n _ _ ∙∙ cong (ΩKn+1→Kn n) helper3 ∙∙ Iso.leftInv (Iso-Kn-ΩKn+1 n) (Fc c)
where
helper3 : (λ i₁ → p i₁ (inl (f c))) ∙ sym (λ i₁ → p i₁ (inr (g c))) ≡ Kn→ΩKn+1 n (Fc c)
helper3 = cong ((λ i₁ → p i₁ (inl (f c))) ∙_) (lUnit _) ∙ sym (PathP→compPathR (cong (λ f → cong f (push c)) p))
Im-Δ⊂Ker-d : (n : ℕ) (a : coHom n C)
→ isInIm (Δ n) a
→ isInKer (d n) a
Im-Δ⊂Ker-d n =
ST.elim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelPath 2 isSetSetTrunc _ _)
λ Fc → PT.rec (isOfHLevelPath' 1 isSetSetTrunc _ _)
(sigmaProdElim (λ _ → isOfHLevelPath 2 isSetSetTrunc _ _)
λ Fa Fb p → PT.rec (isOfHLevelPath' 1 isSetSetTrunc _ _)
(λ q → ((λ i → fst (d n) ∣ (q (~ i)) ∣₂) ∙ dΔ-Id n Fa Fb))
(Iso.fun (PathIdTrunc₀Iso) p))
where
d-preLeftId : (n : ℕ) (Fa : A → coHomK n)(d : (Pushout f g))
→ d-pre n (Fa ∘ f) d ≡ 0ₖ (suc n)
d-preLeftId n Fa (inl x) = Kn→ΩKn+1 n (Fa x)
d-preLeftId n Fa (inr x) = refl
d-preLeftId n Fa (push a i) j = Kn→ΩKn+1 n (Fa (f a)) (j ∨ i)
d-preRightId : (n : ℕ) (Fb : B → coHomK n) (d : (Pushout f g))
→ d-pre n (Fb ∘ g) d ≡ 0ₖ (suc n)
d-preRightId n Fb (inl x) = refl
d-preRightId n Fb (inr x) = sym (Kn→ΩKn+1 n (Fb x))
d-preRightId n Fb (push a i) j = Kn→ΩKn+1 n (Fb (g a)) (~ j ∧ i)
dΔ-Id : (n : ℕ) (Fa : A → coHomK n) (Fb : B → coHomK n)
→ fst (d n) (fst (Δ n) (∣ Fa ∣₂ , ∣ Fb ∣₂)) ≡ 0ₕ (suc n)
dΔ-Id n Fa Fb = -distrLemma n (suc n) (d n) ∣ Fa ∘ f ∣₂ ∣ Fb ∘ g ∣₂
∙∙ (λ i → ∣ (λ x → d-preLeftId n Fa x i) ∣₂ -[ (suc n) ]ₕ ∣ (λ x → d-preRightId n Fb x i) ∣₂)
∙∙ rCancelₕ (suc n) (0ₕ (suc n))