/
has_colimits.lean
408 lines (366 loc) · 14.7 KB
/
has_colimits.lean
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
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
/-
Copyright (c) 2020 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
import algebraic_geometry.presheafed_space
import topology.category.Top.limits.basic
import topology.sheaves.limits
/-!
# `PresheafedSpace C` has colimits.
If `C` has limits, then the category `PresheafedSpace C` has colimits,
and the forgetful functor to `Top` preserves these colimits.
When restricted to a diagram where the underlying continuous maps are open embeddings,
this says that we can glue presheaved spaces.
Given a diagram `F : J ⥤ PresheafedSpace C`,
we first build the colimit of the underlying topological spaces,
as `colimit (F ⋙ PresheafedSpace.forget C)`. Call that colimit space `X`.
Our strategy is to push each of the presheaves `F.obj j`
forward along the continuous map `colimit.ι (F ⋙ PresheafedSpace.forget C) j` to `X`.
Since pushforward is functorial, we obtain a diagram `J ⥤ (presheaf C X)ᵒᵖ`
of presheaves on a single space `X`.
(Note that the arrows now point the other direction,
because this is the way `PresheafedSpace C` is set up.)
The limit of this diagram then constitutes the colimit presheaf.
-/
noncomputable theory
universes v' u' v u
open category_theory
open Top
open Top.presheaf
open topological_space
open opposite
open category_theory.category
open category_theory.limits
open category_theory.functor
variables {J : Type u'} [category.{v'} J]
variables {C : Type u} [category.{v} C]
namespace algebraic_geometry
namespace PresheafedSpace
local attribute [simp] eq_to_hom_map
local attribute [tidy] tactic.auto_cases_opens
@[simp]
lemma map_id_c_app (F : J ⥤ PresheafedSpace.{v} C) (j) (U) :
(F.map (𝟙 j)).c.app (op U) =
(pushforward.id (F.obj j).presheaf).inv.app (op U) ≫
(pushforward_eq (by { simp, refl }) (F.obj j).presheaf).hom.app (op U) :=
begin
cases U,
dsimp,
simp [PresheafedSpace.congr_app (F.map_id j)],
refl,
end
@[simp]
lemma map_comp_c_app (F : J ⥤ PresheafedSpace.{v} C) {j₁ j₂ j₃} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃) (U) :
(F.map (f ≫ g)).c.app (op U) =
(F.map g).c.app (op U) ≫
(pushforward_map (F.map g).base (F.map f).c).app (op U) ≫
(pushforward.comp (F.obj j₁).presheaf (F.map f).base (F.map g).base).inv.app (op U) ≫
(pushforward_eq (by { rw F.map_comp, refl }) _).hom.app _ :=
begin
cases U,
dsimp,
simp only [PresheafedSpace.congr_app (F.map_comp f g)],
dsimp, simp, dsimp, simp, -- See note [dsimp, simp]
end
/--
Given a diagram of `PresheafedSpace C`s, its colimit is computed by pushing the sheaves onto
the colimit of the underlying spaces, and taking componentwise limit.
This is the componentwise diagram for an open set `U` of the colimit of the underlying spaces.
-/
@[simps]
def componentwise_diagram (F : J ⥤ PresheafedSpace.{v} C)
[has_colimit F] (U : opens (limits.colimit F).carrier) : Jᵒᵖ ⥤ C :=
{ obj := λ j, (F.obj (unop j)).presheaf.obj (op ((opens.map (colimit.ι F (unop j)).base).obj U)),
map := λ j k f, (F.map f.unop).c.app _ ≫ (F.obj (unop k)).presheaf.map
(eq_to_hom (by { rw [← colimit.w F f.unop, comp_base], refl })),
map_comp' := λ i j k f g,
begin
cases U,
dsimp,
simp_rw [map_comp_c_app, category.assoc],
congr' 1,
rw [Top.presheaf.pushforward.comp_inv_app, Top.presheaf.pushforward_eq_hom_app,
category_theory.nat_trans.naturality_assoc, Top.presheaf.pushforward_map_app],
congr' 1,
rw [category.id_comp, ← (F.obj (unop k)).presheaf.map_comp],
erw ← (F.obj (unop k)).presheaf.map_comp,
congr
end }
variable [has_colimits_of_shape J Top.{v}]
/--
Given a diagram of presheafed spaces,
we can push all the presheaves forward to the colimit `X` of the underlying topological spaces,
obtaining a diagram in `(presheaf C X)ᵒᵖ`.
-/
@[simps]
def pushforward_diagram_to_colimit (F : J ⥤ PresheafedSpace.{v} C) :
J ⥤ (presheaf C (colimit (F ⋙ PresheafedSpace.forget C)))ᵒᵖ :=
{ obj := λ j, op ((colimit.ι (F ⋙ PresheafedSpace.forget C) j) _* (F.obj j).presheaf),
map := λ j j' f,
(pushforward_map (colimit.ι (F ⋙ PresheafedSpace.forget C) j') (F.map f).c ≫
(pushforward.comp (F.obj j).presheaf ((F ⋙ PresheafedSpace.forget C).map f)
(colimit.ι (F ⋙ PresheafedSpace.forget C) j')).inv ≫
(pushforward_eq (colimit.w (F ⋙ PresheafedSpace.forget C) f) (F.obj j).presheaf).hom).op,
map_id' := λ j,
begin
apply (op_equiv _ _).injective,
ext U,
induction U using opposite.rec,
cases U,
dsimp, simp, dsimp, simp,
end,
map_comp' := λ j₁ j₂ j₃ f g,
begin
apply (op_equiv _ _).injective,
ext U,
dsimp,
simp only [map_comp_c_app, id.def, eq_to_hom_op, pushforward_map_app, eq_to_hom_map, assoc,
id_comp, pushforward.comp_inv_app, pushforward_eq_hom_app],
dsimp,
simp only [eq_to_hom_trans, id_comp],
congr' 1,
-- The key fact is `(F.map f).c.congr`,
-- which allows us in rewrite in the argument of `(F.map f).c.app`.
rw (F.map f).c.congr,
-- Now we pick up the pieces. First, we say what we want to replace that open set by:
swap 3,
refine op ((opens.map (colimit.ι (F ⋙ PresheafedSpace.forget C) j₂)).obj (unop U)),
-- Now we show the open sets are equal.
swap 2,
{ apply unop_injective,
rw ←opens.map_comp_obj,
congr,
exact colimit.w (F ⋙ PresheafedSpace.forget C) g, },
-- Finally, the original goal is now easy:
swap 2,
{ simp, refl, },
end, }
variables [∀ X : Top.{v}, has_limits_of_shape Jᵒᵖ (X.presheaf C)]
/--
Auxiliary definition for `PresheafedSpace.has_colimits`.
-/
def colimit (F : J ⥤ PresheafedSpace.{v} C) : PresheafedSpace C :=
{ carrier := colimit (F ⋙ PresheafedSpace.forget C),
presheaf := limit (pushforward_diagram_to_colimit F).left_op, }
@[simp] lemma colimit_carrier (F : J ⥤ PresheafedSpace.{v} C) :
(colimit F).carrier = limits.colimit (F ⋙ PresheafedSpace.forget C) := rfl
@[simp] lemma colimit_presheaf (F : J ⥤ PresheafedSpace.{v} C) :
(colimit F).presheaf = limit (pushforward_diagram_to_colimit F).left_op := rfl
/--
Auxiliary definition for `PresheafedSpace.has_colimits`.
-/
@[simps]
def colimit_cocone (F : J ⥤ PresheafedSpace.{v} C) : cocone F :=
{ X := colimit F,
ι :=
{ app := λ j,
{ base := colimit.ι (F ⋙ PresheafedSpace.forget C) j,
c := limit.π _ (op j), },
naturality' := λ j j' f,
begin
fapply PresheafedSpace.ext,
{ ext x,
exact colimit.w_apply (F ⋙ PresheafedSpace.forget C) f x, },
{ ext U,
induction U using opposite.rec,
cases U,
dsimp,
simp only [PresheafedSpace.id_c_app, eq_to_hom_op, eq_to_hom_map, assoc,
pushforward.comp_inv_app],
rw ← congr_arg nat_trans.app (limit.w (pushforward_diagram_to_colimit F).left_op f.op),
dsimp,
simp only [eq_to_hom_op, eq_to_hom_map, assoc, id_comp, pushforward.comp_inv_app],
congr,
dsimp,
simp only [id_comp],
simpa, }
end, }, }
variables [has_limits_of_shape Jᵒᵖ C]
namespace colimit_cocone_is_colimit
/--
Auxiliary definition for `PresheafedSpace.colimit_cocone_is_colimit`.
-/
def desc_c_app (F : J ⥤ PresheafedSpace.{v} C) (s : cocone F) (U : (opens ↥(s.X.carrier))ᵒᵖ) :
s.X.presheaf.obj U ⟶
(colimit.desc (F ⋙ PresheafedSpace.forget C)
((PresheafedSpace.forget C).map_cocone s) _*
limit (pushforward_diagram_to_colimit F).left_op).obj
U :=
begin
refine
limit.lift _ { X := s.X.presheaf.obj U, π := { app := λ j, _, naturality' := λ j j' f, _, }} ≫
(limit_obj_iso_limit_comp_evaluation _ _).inv,
-- We still need to construct the `app` and `naturality'` fields omitted above.
{ refine (s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eq_to_hom _),
dsimp,
rw ←opens.map_comp_obj,
simp, },
{ rw (PresheafedSpace.congr_app (s.w f.unop).symm U),
dsimp,
have w := functor.congr_obj (congr_arg opens.map
(colimit.ι_desc ((PresheafedSpace.forget C).map_cocone s) (unop j))) (unop U),
simp only [opens.map_comp_obj_unop] at w,
replace w := congr_arg op w,
have w' := nat_trans.congr (F.map f.unop).c w,
rw w',
dsimp, simp, dsimp, simp, },
end
lemma desc_c_naturality (F : J ⥤ PresheafedSpace.{v} C) (s : cocone F)
{U V : (opens ↥(s.X.carrier))ᵒᵖ} (i : U ⟶ V) :
s.X.presheaf.map i ≫ desc_c_app F s V =
desc_c_app F s U ≫ (colimit.desc (F ⋙ forget C)
((forget C).map_cocone s) _* (colimit_cocone F).X.presheaf).map i :=
begin
dsimp [desc_c_app],
ext,
simp only [limit.lift_π, nat_trans.naturality, limit.lift_π_assoc, eq_to_hom_map, assoc,
pushforward_obj_map, nat_trans.naturality_assoc, op_map,
limit_obj_iso_limit_comp_evaluation_inv_π_app_assoc,
limit_obj_iso_limit_comp_evaluation_inv_π_app],
dsimp,
have w := functor.congr_hom (congr_arg opens.map
(colimit.ι_desc ((PresheafedSpace.forget C).map_cocone s) (unop j))) (i.unop),
simp only [opens.map_comp_map] at w,
replace w := congr_arg quiver.hom.op w,
rw w,
dsimp, simp,
end
/--
Auxiliary definition for `PresheafedSpace.colimit_cocone_is_colimit`.
-/
def desc (F : J ⥤ PresheafedSpace.{v} C) (s : cocone F) : colimit F ⟶ s.X :=
{ base := colimit.desc (F ⋙ PresheafedSpace.forget C) ((PresheafedSpace.forget C).map_cocone s),
c :=
{ app := λ U, desc_c_app F s U,
naturality' := λ U V i, desc_c_naturality F s i } }
lemma desc_fac (F : J ⥤ PresheafedSpace.{v} C) (s : cocone F) (j : J) :
(colimit_cocone F).ι.app j ≫ desc F s = s.ι.app j :=
begin
fapply PresheafedSpace.ext,
{ simp [desc] },
{ ext,
dsimp [desc, desc_c_app],
simpa }
end
end colimit_cocone_is_colimit
open colimit_cocone_is_colimit
/--
Auxiliary definition for `PresheafedSpace.has_colimits`.
-/
def colimit_cocone_is_colimit (F : J ⥤ PresheafedSpace.{v} C) : is_colimit (colimit_cocone F) :=
{ desc := λ s, desc F s,
fac' := λ s, desc_fac F s,
uniq' := λ s m w,
begin
-- We need to use the identity on the continuous maps twice, so we prepare that first:
have t : m.base = colimit.desc (F ⋙ PresheafedSpace.forget C)
((PresheafedSpace.forget C).map_cocone s),
{ apply category_theory.limits.colimit.hom_ext, intros j,
apply continuous_map.ext, intros x,
dsimp,
simp only [colimit.ι_desc_apply, map_cocone_ι_app],
rw ← w j,
simp, },
fapply PresheafedSpace.ext, -- could `ext` please not reorder goals?
{ exact t, },
{ ext U j, dsimp [desc, desc_c_app],
simp only [limit.lift_π, eq_to_hom_op, eq_to_hom_map, assoc,
limit_obj_iso_limit_comp_evaluation_inv_π_app],
rw PresheafedSpace.congr_app (w (unop j)).symm U,
dsimp,
have w := congr_arg op (functor.congr_obj (congr_arg opens.map t) (unop U)),
rw nat_trans.congr (limit.π (pushforward_diagram_to_colimit F).left_op j) w,
simp }
end, }
instance : has_colimits_of_shape J (PresheafedSpace.{v} C) :=
{ has_colimit := λ F, has_colimit.mk
{ cocone := colimit_cocone F,
is_colimit := colimit_cocone_is_colimit F } }
instance : preserves_colimits_of_shape J (PresheafedSpace.forget C) :=
{ preserves_colimit := λ F, preserves_colimit_of_preserves_colimit_cocone
(colimit_cocone_is_colimit F)
begin
apply is_colimit.of_iso_colimit (colimit.is_colimit _),
fapply cocones.ext,
{ refl, },
{ intro j, dsimp, simp, }
end }
/--
When `C` has limits, the category of presheaved spaces with values in `C` itself has colimits.
-/
instance [has_limits C] : has_colimits (PresheafedSpace.{v} C) :=
{ has_colimits_of_shape := λ J 𝒥, by exactI
{ has_colimit := λ F, has_colimit.mk
{ cocone := colimit_cocone F,
is_colimit := colimit_cocone_is_colimit F } } }
/--
The underlying topological space of a colimit of presheaved spaces is
the colimit of the underlying topological spaces.
-/
instance forget_preserves_colimits [has_limits C] : preserves_colimits (PresheafedSpace.forget C) :=
{ preserves_colimits_of_shape := λ J 𝒥, by exactI
{ preserves_colimit := λ F, preserves_colimit_of_preserves_colimit_cocone
(colimit_cocone_is_colimit F)
begin
apply is_colimit.of_iso_colimit (colimit.is_colimit _),
fapply cocones.ext,
{ refl, },
{ intro j, dsimp, simp, }
end } }
/--
The components of the colimit of a diagram of `PresheafedSpace C` is obtained
via taking componentwise limits.
-/
def colimit_presheaf_obj_iso_componentwise_limit (F : J ⥤ PresheafedSpace.{v} C) [has_colimit F]
(U : opens (limits.colimit F).carrier) :
(limits.colimit F).presheaf.obj (op U) ≅ limit (componentwise_diagram F U) :=
begin
refine ((sheaf_iso_of_iso (colimit.iso_colimit_cocone
⟨_, colimit_cocone_is_colimit F⟩).symm).app (op U)).trans _,
refine (limit_obj_iso_limit_comp_evaluation _ _).trans (limits.lim.map_iso _),
fapply nat_iso.of_components,
{ intro X,
refine ((F.obj (unop X)).presheaf.map_iso (eq_to_iso _)),
simp only [functor.op_obj, unop_op, op_inj_iff, opens.map_coe, set_like.ext'_iff,
set.preimage_preimage],
simp_rw ← comp_app,
congr' 2,
exact ι_preserves_colimits_iso_inv (forget C) F (unop X) },
{ intros X Y f,
change ((F.map f.unop).c.app _ ≫ _ ≫ _) ≫ (F.obj (unop Y)).presheaf.map _ = _ ≫ _,
rw Top.presheaf.pushforward.comp_inv_app,
erw category.id_comp,
rw category.assoc,
erw [← (F.obj (unop Y)).presheaf.map_comp, (F.map f.unop).c.naturality_assoc,
← (F.obj (unop Y)).presheaf.map_comp],
congr }
end
@[simp]
lemma colimit_presheaf_obj_iso_componentwise_limit_inv_ι_app (F : J ⥤ PresheafedSpace.{v} C)
(U : opens (limits.colimit F).carrier) (j : J) :
(colimit_presheaf_obj_iso_componentwise_limit F U).inv ≫ (colimit.ι F j).c.app (op U) =
limit.π _ (op j) :=
begin
delta colimit_presheaf_obj_iso_componentwise_limit,
rw [iso.trans_inv, iso.trans_inv, iso.app_inv, sheaf_iso_of_iso_inv, pushforward_to_of_iso_app,
congr_app (iso.symm_inv _)],
simp_rw category.assoc,
rw [← functor.map_comp_assoc, nat_trans.naturality],
erw ← comp_c_app_assoc,
rw congr_app (colimit.iso_colimit_cocone_ι_hom _ _),
simp_rw category.assoc,
erw [limit_obj_iso_limit_comp_evaluation_inv_π_app_assoc, lim_map_π_assoc],
convert category.comp_id _,
erw ← (F.obj j).presheaf.map_id,
iterate 2 { erw ← (F.obj j).presheaf.map_comp },
congr
end
@[simp]
lemma colimit_presheaf_obj_iso_componentwise_limit_hom_π (F : J ⥤ PresheafedSpace.{v} C)
(U : opens (limits.colimit F).carrier) (j : J) :
(colimit_presheaf_obj_iso_componentwise_limit F U).hom ≫ limit.π _ (op j) =
(colimit.ι F j).c.app (op U) :=
by rw [← iso.eq_inv_comp, colimit_presheaf_obj_iso_componentwise_limit_inv_ι_app]
end PresheafedSpace
end algebraic_geometry