/
stalks.lean
69 lines (55 loc) · 2.04 KB
/
stalks.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
/-
Copyright (c) 2019 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.sheaves.stalks
/-!
# Stalks for presheaved spaces
This file lifts constructions of stalks and pushforwards of stalks to work with
the category of presheafed spaces.
-/
universes v u v' u'
open category_theory
open category_theory.limits category_theory.category category_theory.functor
open algebraic_geometry
open topological_space
variables {C : Type u} [category.{v} C] [has_colimits C]
local attribute [tidy] tactic.op_induction'
open Top.presheaf
namespace algebraic_geometry.PresheafedSpace
def stalk (X : PresheafedSpace C) (x : X) : C := X.𝒪.stalk x
def stalk_map {X Y : PresheafedSpace C} (α : X ⟶ Y) (x : X) : Y.stalk (α.base x) ⟶ X.stalk x :=
(stalk_functor C (α.base x)).map (α.c) ≫ X.𝒪.stalk_pushforward C α.base x
namespace stalk_map
@[simp] lemma id (X : PresheafedSpace C) (x : X) : stalk_map (𝟙 X) x = 𝟙 (X.stalk x) :=
begin
dsimp [stalk_map],
simp only [stalk_pushforward.id],
rw [←map_comp],
convert (stalk_functor C x).map_id X.𝒪,
tidy,
end
-- TODO understand why this proof is still gross (i.e. requires using `erw`)
@[simp] lemma comp {X Y Z : PresheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (x : X) :
stalk_map (α ≫ β) x =
(stalk_map β (α.base x) : Z.stalk (β.base (α.base x)) ⟶ Y.stalk (α.base x)) ≫
(stalk_map α x : Y.stalk (α.base x) ⟶ X.stalk x) :=
begin
dsimp [stalk_map, stalk_functor, stalk_pushforward],
ext U,
op_induction U,
cases U,
simp only [colimit.ι_map_assoc, colimit.ι_pre_assoc, colimit.ι_pre,
whisker_left_app, whisker_right_app,
assoc, id_comp, map_id, map_comp],
dsimp,
simp only [map_id, assoc, pushforward.comp_inv_app],
-- FIXME Why doesn't simp do this:
erw [category_theory.functor.map_id],
erw [category_theory.functor.map_id],
erw [id_comp, id_comp, id_comp],
end
end stalk_map
end algebraic_geometry.PresheafedSpace