|
1 | 1 | /- |
2 | 2 | Copyright (c) 2019 Scott Morrison. All rights reserved. |
3 | 3 | Released under Apache 2.0 license as described in the file LICENSE. |
4 | | -Authors: Scott Morrison |
| 4 | +Authors: Scott Morrison, Justus Springer |
5 | 5 | -/ |
6 | 6 | import topology.category.Top.open_nhds |
7 | 7 | import topology.sheaves.presheaf |
| 8 | +import topology.sheaves.sheaf_condition.unique_gluing |
8 | 9 | import category_theory.limits.types |
9 | 10 |
|
| 11 | +/-! |
| 12 | +# Stalks |
| 13 | +
|
| 14 | +For a presheaf `F` on a topological space `X`, valued in some category `C`, the *stalk* of `F` |
| 15 | +at the point `x : X` is defined as the colimit of the following functor |
| 16 | +
|
| 17 | +(nhds x)ᵒᵖ ⥤ (opens X)ᵒᵖ ⥤ C |
| 18 | +
|
| 19 | +where the functor on the left is the inclusion of categories and the functor on the right is `F`. |
| 20 | +For an open neighborhood `U` of `x`, we define the map `F.germ x : F.obj (op U) ⟶ F.stalk x` as the |
| 21 | +canonical morphism into this colimit. |
| 22 | +
|
| 23 | +Taking stalks is functorial: For every point `x : X` we define a functor `stalk_functor C x`, |
| 24 | +sending presheaves on `X` to objects of `C`. In `is_iso_iff_stalk_functor_map_iso`, we prove that a |
| 25 | +map `f : F ⟶ G` between `Type`-valued sheaves is an isomorphism if and only if all the maps |
| 26 | +`F.stalk x ⟶ G.stalk x` (given by the stalk functor on `f`) are isomorphisms. |
| 27 | +
|
| 28 | +For a map `f : X ⟶ Y` between topological spaces, we define `stalk_pushforward` as the induced map |
| 29 | +on the stalks `(f _* ℱ).stalk (f x) ⟶ ℱ.stalk x`. |
| 30 | +
|
| 31 | +-/ |
| 32 | + |
10 | 33 | noncomputable theory |
11 | 34 |
|
12 | 35 | universes v u v' u' |
@@ -109,6 +132,173 @@ lemma stalk_hom_ext (F : X.presheaf C) {x} {Y : C} {f₁ f₂ : F.stalk x ⟶ Y} |
109 | 132 | (ih : ∀ (U : opens X) (hxU : x ∈ U), F.germ ⟨x, hxU⟩ ≫ f₁ = F.germ ⟨x, hxU⟩ ≫ f₂) : f₁ = f₂ := |
110 | 133 | colimit.hom_ext $ λ U, by { op_induction U, cases U with U hxU, exact ih U hxU } |
111 | 134 |
|
| 135 | +/-- If two sections agree on all stalks, they must be equal -/ |
| 136 | +lemma section_ext (F : sheaf (Type v) X) (U : opens X) (s t : F.presheaf.obj (op U)) : |
| 137 | + (∀ x : U, F.presheaf.germ x s = F.presheaf.germ x t) → s = t := |
| 138 | +begin |
| 139 | + intro h, |
| 140 | + -- We use `germ_eq` and the axiom of choice, to pick for every point `x` a neighbourhood |
| 141 | + -- `V`, such that the restrictions of `s` and `t` to `V` coincide. Since a restriction |
| 142 | + -- map `V ⟶ U` is *data* (lives in `Type`, not `Prop`), we encode all of this as a dependent |
| 143 | + -- pair (sigma type) |
| 144 | + let V : Π (x : U), Σ (V : open_nhds x.1), |
| 145 | + { iVU : V.1 ⟶ U // F.presheaf.map iVU.op s = F.presheaf.map iVU.op t } := λ x, by { |
| 146 | + choose V m iVU₀ iVU₁ heq using (F.presheaf.germ_eq x.1 x.2 x.2 s t (h x)), |
| 147 | + refine ⟨⟨V,m⟩,iVU₀,_⟩, |
| 148 | + convert heq, |
| 149 | + }, |
| 150 | + refine F.eq_of_locally_eq' (λ x, (V x).1.1) U (λ x, (V x).2.1) _ s t (λ x, (V x).2.2), |
| 151 | + -- Here, it remains to show that the choosen neighborhoods really define a cover of `U` |
| 152 | + intros x hxU, |
| 153 | + rw [subtype.val_eq_coe, opens.mem_coe, opens.mem_supr], |
| 154 | + exact ⟨⟨x,hxU⟩,(V ⟨x,hxU⟩).1.2⟩, |
| 155 | +end |
| 156 | + |
| 157 | +@[simp, reassoc] lemma stalk_functor_map_germ {F G : X.presheaf C} (U : opens X) (x : U) |
| 158 | + (f : F ⟶ G) : germ F x ≫ (stalk_functor C x.1).map f = f.app (op U) ≫ germ G x := |
| 159 | +colimit.ι_map (whisker_left ((open_nhds.inclusion x.1).op) f) (op ⟨U, x.2⟩) |
| 160 | + |
| 161 | +@[simp] lemma stalk_functor_map_germ_apply (U : opens X) (x : U) {F G : X.presheaf (Type v)} |
| 162 | + (f : F ⟶ G) (s : F.obj (op U)) : |
| 163 | + (stalk_functor (Type v) x.1).map f (germ F x s) = germ G x (f.app (op U) s) := |
| 164 | +congr_fun (stalk_functor_map_germ U x f) s |
| 165 | + |
| 166 | +open function |
| 167 | + |
| 168 | +lemma stalk_functor_map_injective_of_app_injective {F G : presheaf (Type v) X} (f : F ⟶ G) |
| 169 | + (h : ∀ U : opens X, injective (f.app (op U))) (x : X) : |
| 170 | + injective ((stalk_functor (Type v) x).map f) := λ s t hst, |
| 171 | +begin |
| 172 | + rcases germ_exist F x s with ⟨U₁, hxU₁, s, rfl⟩, |
| 173 | + rcases germ_exist F x t with ⟨U₂, hxU₂, t, rfl⟩, |
| 174 | + simp only [stalk_functor_map_germ_apply _ ⟨x,_⟩] at hst, |
| 175 | + obtain ⟨W, hxW, iWU₁, iWU₂, heq⟩ := G.germ_eq x hxU₁ hxU₂ _ _ hst, |
| 176 | + rw [← functor_to_types.naturality, ← functor_to_types.naturality] at heq, |
| 177 | + replace heq := h W heq, |
| 178 | + convert congr_arg (F.germ ⟨x,hxW⟩) heq, |
| 179 | + exacts [(F.germ_res_apply iWU₁ ⟨x,hxW⟩ s).symm, |
| 180 | + (F.germ_res_apply iWU₂ ⟨x,hxW⟩ t).symm], |
| 181 | +end |
| 182 | + |
| 183 | +/- |
| 184 | +Note that the analogous statement for surjectivity is false: Surjectivity on stalks does not |
| 185 | +imply surjectivity of the components of a sheaf morphism. However it does imply that the morphism |
| 186 | +is an epi, but this fact is not yet formalized. |
| 187 | +-/ |
| 188 | +lemma app_injective_of_stalk_functor_map_injective {F : sheaf (Type v) X} {G : presheaf (Type v) X} |
| 189 | + (f : F.presheaf ⟶ G) (h : ∀ x : X, injective ((stalk_functor (Type v) x).map f)) (U : opens X) : |
| 190 | + injective (f.app (op U)) := λ s t hst, |
| 191 | +begin |
| 192 | + apply section_ext, |
| 193 | + intro x, |
| 194 | + apply h x.1, |
| 195 | + simp only [stalk_functor_map_germ_apply, hst], |
| 196 | +end |
| 197 | + |
| 198 | +lemma app_injective_iff_stalk_functor_map_injective {F : sheaf (Type v) X} |
| 199 | + {G : presheaf (Type v) X} (f : F.presheaf ⟶ G) : |
| 200 | + (∀ x : X, injective ((stalk_functor (Type v) x).map f)) ↔ |
| 201 | + (∀ U : opens X, injective (f.app (op U))) := |
| 202 | +⟨app_injective_of_stalk_functor_map_injective f, stalk_functor_map_injective_of_app_injective f⟩ |
| 203 | + |
| 204 | +lemma app_bijective_of_stalk_functor_map_bijective {F G : sheaf (Type v) X} (f : F ⟶ G) |
| 205 | + (h : ∀ x : X, bijective ((stalk_functor (Type v) x).map f)) (U : opens X) : |
| 206 | + bijective (f.app (op U)) := |
| 207 | +begin |
| 208 | + -- We already know that `f.app (op U)` is injective. We save that fact here as we will |
| 209 | + -- need it again later. |
| 210 | + have h_inj := app_injective_of_stalk_functor_map_injective f (λ x, (h x).1), |
| 211 | + refine ⟨h_inj U, (λ t,_)⟩, |
| 212 | + -- For surjectivity, we are given an arbitrary section `t` and need to find a preimage for it. |
| 213 | + -- First, we show that we can find preimages *locally*. That is, for each `x : U` we construct |
| 214 | + -- neighborhood `V ≤ U` and a section `s : F.obj (op V))` such that `f.app (op V) s` and `t` |
| 215 | + -- agree on `V`. |
| 216 | + have exists_local_preim : ∀ x : U, ∃ (V : open_nhds x.1) (iVU : V.1 ⟶ U) |
| 217 | + (s : F.presheaf.obj (op V.1)), f.app (op V.1) s = G.presheaf.map iVU.op t := λ x, by { |
| 218 | + -- Since `f` is surjective on stalks, we can find a preimage `s₀` of the germ of `t` |
| 219 | + obtain ⟨s₀,hs₀⟩ := (h x).2 (G.presheaf.germ x t), |
| 220 | + -- ... and this preimage must come from some section `s₁` |
| 221 | + obtain ⟨V₁,hxV₁,s₁,hs₁⟩ := F.presheaf.germ_exist x.1 s₀, |
| 222 | + subst hs₁, rename hs₀ hs₁, |
| 223 | + erw stalk_functor_map_germ_apply V₁ ⟨x.1,hxV₁⟩ f s₁ at hs₁, |
| 224 | + -- Now, the germ of `f.app (op V₁) s₁` equals the germ of `t`, hence they must coincide on |
| 225 | + -- some open neighborhood |
| 226 | + obtain ⟨V₂,hxV₂, iV₂V₁, iV₂U, heq⟩ := G.presheaf.germ_eq x.1 hxV₁ x.2 _ _ hs₁, |
| 227 | + -- The restriction of `s₁` to that neighborhood is our desired local preimage |
| 228 | + let s₂ := F.presheaf.map iV₂V₁.op s₁, |
| 229 | + use [V₂,hxV₂,iV₂U,s₂], |
| 230 | + rwa functor_to_types.naturality }, |
| 231 | + -- Now, we use the axiom of choice to create a function `local_preim` giving us for each point |
| 232 | + -- `x : U` a neighborhood `V` and a local preimage for `t` on `V`. |
| 233 | + have local_preim : Π x : U, Σ (V : open_nhds x.1) (iVU : V.1 ⟶ U), |
| 234 | + {s : F.presheaf.obj (op V.1) // f.app (op V.1) s = G.presheaf.map iVU.op t } := λ x, by { |
| 235 | + choose V iVU s heq using exists_local_preim x, |
| 236 | + exact ⟨V,iVU,s,heq⟩ }, |
| 237 | + clear exists_local_preim, |
| 238 | + -- In particular, we obtain a covering family of opens and a family of sections |
| 239 | + let V : U → opens X := λ x, (local_preim x).1.1, |
| 240 | + let sf : Π x : U, F.presheaf.obj (op (V x)) := λ x, (local_preim x).2.2.1, |
| 241 | + have V_cover : U ≤ supr V := λ x hx, by { |
| 242 | + rw [subtype.val_eq_coe, opens.mem_coe, opens.mem_supr], |
| 243 | + exact ⟨⟨x,hx⟩,(local_preim _).1.2⟩ }, |
| 244 | + -- Using this data, we can glue all of the local preimages together, giving us our candidate |
| 245 | + -- for the preimage of `t` |
| 246 | + obtain ⟨s, s_spec, -⟩ := F.exists_unique_gluing' V U (λ x, (local_preim x).2.1) V_cover sf _, |
| 247 | + use s, |
| 248 | + -- Note that we generated an additional goal: We need to show that our family of sections `sf` |
| 249 | + -- is actually compatible. We get that out of the way first. |
| 250 | + swap, |
| 251 | + { intros x y, |
| 252 | + -- The only thing we know about the sections `sf` is that their image under `f` equals (the |
| 253 | + -- restriction of) `t`. It is at this point that we need injectivity of `f` again! |
| 254 | + apply h_inj, |
| 255 | + -- Here, both sides are equal to a restriction of `t` |
| 256 | + transitivity ; |
| 257 | + erw [functor_to_types.naturality, (local_preim _).2.2.2, ← functor_to_types.map_comp_apply], |
| 258 | + refl }, |
| 259 | + -- The only thing left to prove is that `s` really is a preimage of `t` |
| 260 | + -- Of course, we show the equality locally |
| 261 | + apply G.eq_of_locally_eq' V U (λ x, (local_preim x).2.1) V_cover, |
| 262 | + intro x, |
| 263 | + convert congr_arg (f.app (op (V x))) (s_spec x), |
| 264 | + exacts [(functor_to_types.naturality _ _ f _ _).symm, (local_preim x).2.2.2.symm], |
| 265 | +end |
| 266 | + |
| 267 | +/-- |
| 268 | +If all the stalk maps of map `f : F ⟶ G` of `Type`-valued sheaves are isomorphisms, then `f` is |
| 269 | +an isomorphism. |
| 270 | +-/ |
| 271 | +-- Making this an instance would cause a loop in typeclass resolution with `functor.map_is_iso` |
| 272 | +lemma is_iso_of_stalk_functor_map_iso {F G : sheaf (Type v) X} (f : F ⟶ G) |
| 273 | + [∀ x : X, is_iso ((stalk_functor (Type v) x).map f)] : is_iso f := |
| 274 | +begin |
| 275 | + -- Rather annoyingly, an isomorphism of presheaves isn't quite the same as an isomorphism of |
| 276 | + -- sheaves. We have to use that the induced functor from sheaves to presheaves is fully faithful |
| 277 | + haveI : is_iso ((induced_functor sheaf.presheaf).map f) := |
| 278 | + @nat_iso.is_iso_of_is_iso_app _ _ _ _ F.presheaf G.presheaf f (by { |
| 279 | + intro U, op_induction U, |
| 280 | + rw is_iso_iff_bijective, |
| 281 | + exact app_bijective_of_stalk_functor_map_bijective f |
| 282 | + (λ x, (is_iso_iff_bijective _).mp (_inst_3 x)) U, |
| 283 | + }), |
| 284 | + exact is_iso_of_fully_faithful (induced_functor sheaf.presheaf) f, |
| 285 | +end |
| 286 | + |
| 287 | +/-- |
| 288 | +A morphism of `Type`-valued sheaves `f : F ⟶ G` is an isomorphism if and only if all the stalk |
| 289 | +maps are isomorphisms |
| 290 | +-/ |
| 291 | +lemma is_iso_iff_stalk_functor_map_iso {F G : sheaf (Type v) X} (f : F ⟶ G) : |
| 292 | + is_iso f ↔ ∀ x : X, is_iso ((stalk_functor (Type v) x).map f) := |
| 293 | +begin |
| 294 | + split, |
| 295 | + { intros h x, resetI, |
| 296 | + exact @functor.map_is_iso _ _ _ _ _ _ (stalk_functor (Type v) x) f |
| 297 | + ((induced_functor sheaf.presheaf).map_is_iso f) }, |
| 298 | + { intro h, resetI, |
| 299 | + exact is_iso_of_stalk_functor_map_iso f } |
| 300 | +end |
| 301 | + |
112 | 302 | variables (C) |
113 | 303 |
|
114 | 304 | def stalk_pushforward (f : X ⟶ Y) (ℱ : X.presheaf C) (x : X) : (f _* ℱ).stalk (f x) ⟶ ℱ.stalk x := |
@@ -174,4 +364,5 @@ begin |
174 | 364 | end |
175 | 365 |
|
176 | 366 | end stalk_pushforward |
| 367 | + |
177 | 368 | end Top.presheaf |
0 commit comments