[Merged by Bors] - feat(topology/sheaves): Induced map on stalks

src/topology/sheaves/sheaf_condition/unique_gluing.lean

@@ -5,6 +5,7 @@ Authors: Justus Springer
 -/
 import topology.sheaves.sheaf
 import category_theory.limits.shapes.types
+import category_theory.types
 
 /-!
 # The sheaf condition for a type-valued presheaf
@@ -177,8 +178,7 @@ def sheaf_condition_unique_gluing_of_sheaf_condition :
     choose gl gl_spec gl_uniq using types.unique_of_type_equalizer _ _ (Fsh U) sf' hsf',
     refine eq.trans (gl_uniq s.1 _) (gl_uniq t.1 _).symm ;
       rw [← is_gluing_iff_eq_res F U _ _, inv_hom_id_apply],
-    { exact s.2 },
-    { exact t.2 }
+    exacts [s.2, t.2]
   end
 }
 
@@ -211,8 +211,7 @@ sheaf_condition_of_sheaf_condition_unique_gluing F $ λ ι U sf hsf,
     ext,
     choose gl gl_spec gl_uniq using h U sf hsf,
     refine eq.trans (gl_uniq s.1 _) (gl_uniq t.1 _).symm,
-    { exact s.2 },
-    { exact t.2 }
+    exacts [s.2, t.2]
   },
 }
 
@@ -221,22 +220,74 @@ end presheaf
 
 namespace sheaf
 open presheaf
+open category_theory
 
 variables {X : Top.{u}} (F : sheaf (Type u) X) {ι : Type u} (U : ι → opens X)
 
 /--
 A more convenient way of obtaining a unique gluing of sections for a sheaf
 -/
 lemma exists_unique_gluing (sf : Π i : ι, F.presheaf.obj (op (U i)))
- (hsf : is_compatible F.presheaf U sf) :
- ∃! s : F.presheaf.obj (op (supr U)), is_gluing F.presheaf U sf s  :=
+  (h : is_compatible F.presheaf U sf ) :
+  ∃! s : F.presheaf.obj (op (supr U)), is_gluing F.presheaf U sf s :=
 begin
-  have := (sheaf_condition_unique_gluing_of_sheaf_condition _ F.sheaf_condition U sf hsf),
+  have := (sheaf_condition_unique_gluing_of_sheaf_condition _ F.sheaf_condition U sf h),
   refine ⟨this.default.1,this.default.2,_⟩,
   intros s hs,
   exact congr_arg subtype.val (this.uniq ⟨s,hs⟩),
 end
 
+/--
+In this version of the lemma, the inclusion homs `iUV` can be specified directly by the user,
+which can be more convenient in practice.
+-/
+lemma exists_unique_gluing' (V : opens X) (iUV : Π i : ι, U i ⟶ V) (hcover : V ≤ supr U)
+  (sf : Π i : ι, F.presheaf.obj (op (U i))) (h : is_compatible F.presheaf U sf) :
+  ∃! s : F.presheaf.obj (op V), ∀ i : ι, F.presheaf.map (iUV i).op s = sf i :=
+begin
+  have V_eq_supr_U : V = supr U := le_antisymm hcover (supr_le (λ i, le_of_hom (iUV i))),
+  obtain ⟨gl, gl_spec, gl_uniq⟩ := F.exists_unique_gluing U sf h,
+  refine ⟨F.presheaf.map (eq_to_hom V_eq_supr_U).op gl, (λ i,_), (λ gl' gl'_spec,_)⟩,
+  { rw ← functor_to_types.map_comp_apply,
+    exact gl_spec i },
+  { convert congr_arg _ (gl_uniq (F.presheaf.map (eq_to_hom V_eq_supr_U.symm).op gl') (λ i,_)) ;
+      rw ← functor_to_types.map_comp_apply,
+    { exact (functor_to_types.map_id_apply _ _).symm },
+    { convert gl'_spec i }}
+end
+
+@[ext]
+lemma eq_of_locally_eq (s t : F.presheaf.obj (op (supr U)))
+  (h : ∀ i, F.presheaf.map (opens.le_supr U i).op s = F.presheaf.map (opens.le_supr U i).op t) :
+  s = t :=
+begin
+  apply (mono_iff_injective _).mp (mono_of_is_limit_parallel_pair (F.sheaf_condition U)),
+  ext,
+  dsimp [sheaf_condition_equalizer_products.res],
+  simp,
+  apply h,
+end
+
+/--
+In this version of the lemma, the inclusion homs `iUV` can be specified directly by the user,
+which can be more convenient in practice.
+-/
+lemma eq_of_locally_eq' (V : opens X) (iUV : Π i : ι, U i ⟶ V) (hcover : V ≤ supr U)
+  (s t : F.presheaf.obj (op V))
+  (h : ∀ i, F.presheaf.map (iUV i).op s = F.presheaf.map (iUV i).op t) : s = t :=
+begin
+  have V_eq_supr_U : V = supr U := le_antisymm hcover (supr_le (λ i, le_of_hom (iUV i))),
+  suffices : F.presheaf.map (eq_to_hom V_eq_supr_U.symm).op s =
+             F.presheaf.map (eq_to_hom V_eq_supr_U.symm).op t,
+  { convert congr_arg (F.presheaf.map (eq_to_hom V_eq_supr_U).op) this ;
+    rw ← functor_to_types.map_comp_apply ;
+    exact (functor_to_types.map_id_apply _ _).symm },
+  apply eq_of_locally_eq,
+  intro i,
+  rw [← functor_to_types.map_comp_apply, ← functor_to_types.map_comp_apply],
+  convert h i
+end
+
 end sheaf
 
 end Top

src/topology/sheaves/stalks.lean

@@ -1,12 +1,35 @@
 /-
 Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Scott Morrison, Justus Springer
 -/
 import topology.category.Top.open_nhds
 import topology.sheaves.presheaf
+import topology.sheaves.sheaf_condition.unique_gluing
 import category_theory.limits.types
 
+/-!
+# Stalks
+
+For a presheaf `F` on a topological space `X`, valued in some category `C`, the *stalk* of `F`
+at the point `x : X` is defined as the colimit of the following functor
+
+(nhds x)ᵒᵖ ⥤ (opens X)ᵒᵖ ⥤ C
+
+where the functor on the left is the inclusion of categories and the functor on the right is `F`.
+For an open neighborhood `U` of `x`, we define the map `F.germ x : F.obj (op U) ⟶ F.stalk x` as the
+canonical morphism into this colimit.
+
+For a map `f : X ⟶ Y` between topological spaces, we define `stalk_pushforward` as the induced map
+on the stalks `(f _* ℱ).stalk (f x) ⟶ ℱ.stalk x`.
+
+Furthermore, for a morphism of presheaves `f : F ⟶ G` (over a fixed space `X`), we define
+`stalk_map x f` as the induced map on the stalks `F.stalk x ⟶ G.stalk x`. For a map between
+`Type`-valued sheaves, we show in `is_iso_of_stalk_maps_iso` that if all stalk_maps of `f` are
+isomorphisms, then `f` must be an isomorphism.
+
+-/
+
 noncomputable theory
 
 universes v u v' u'
@@ -109,6 +132,28 @@ lemma stalk_hom_ext (F : X.presheaf C) {x} {Y : C} {f₁ f₂ : F.stalk x ⟶ Y}
   (ih : ∀ (U : opens X) (hxU : x ∈ U), F.germ ⟨x, hxU⟩ ≫ f₁ = F.germ ⟨x, hxU⟩ ≫ f₂) : f₁ = f₂ :=
 colimit.hom_ext $ λ U, by { op_induction U, cases U with U hxU, exact ih U hxU }
 
+/-- If two sections agree on all stalks, they must be equal -/
+lemma section_ext (F : sheaf (Type v) X) (U : opens X) (s t : F.presheaf.obj (op U)) :
+  (∀ x : U, F.presheaf.germ x s = F.presheaf.germ x t) → s = t :=
+begin
+  intro h,
+  -- We use `germ_eq` and the axiom of choice, to pick for every point `x` a neighbourhood
+  -- `V`, such that the restrictions of `s` and `t` to `V` coincide. Since a restriction
+  -- map `V ⟶ U` is *data* (lives in `Type`, not `Prop`), we encode all of this as a dependent
+  -- pair (sigma type)
+  let V : Π (x : U), Σ (V : open_nhds x.1),
+      { iVU : V.1 ⟶ U // F.presheaf.map iVU.op s = F.presheaf.map iVU.op t } := λ x, by {
+    choose V m iVU₀ iVU₁ heq using (F.presheaf.germ_eq x.1 x.2 x.2 s t (h x)),
+    refine ⟨⟨V,m⟩,iVU₀,_⟩,
+    convert heq,
+  },
+  refine F.eq_of_locally_eq' (λ x, (V x).1.1) U (λ x, (V x).2.1) _ s t (λ x, (V x).2.2),
+  -- Here, it remains to show that the choosen neighborhoods really define a cover of `U`
+  intros x hxU,
+  rw [subtype.val_eq_coe, opens.mem_coe, opens.mem_supr],
+  exact ⟨⟨x,hxU⟩,(V ⟨x,hxU⟩).1.2⟩,
+end
+
 variables (C)
 
 def stalk_pushforward (f : X ⟶ Y) (ℱ : X.presheaf C) (x : X) : (f _* ℱ).stalk (f x) ⟶ ℱ.stalk x :=
@@ -174,4 +219,175 @@ begin
 end
 
 end stalk_pushforward
+
+variables {C}
+
+/--
+The induced map of a morphism `f : F ⟶ G` of presheaves on the stalks
+-/
+def stalk_map (x : X) {F G : X.presheaf C} (f : F ⟶ G): F.stalk x ⟶ G.stalk x :=
+(stalk_functor C x).map f
+
+namespace stalk_map
+
+@[simp, reassoc] lemma germ_comp {F G : X.presheaf C} (U : opens X) (x : U) (f : F ⟶ G) :
+  germ F x ≫ stalk_map x.1 f = f.app (op U) ≫ germ G x :=
+colimit.ι_map (whisker_left ((open_nhds.inclusion x.1).op) f) (op ⟨U, x.2⟩)
+
+@[simp] lemma germ_comp_apply (U : opens X) (x : U) {F G : X.presheaf (Type v)} (f : F ⟶ G)
+  (s : F.obj (op U)) :
+  stalk_map x.1 f (germ F x s) = germ G x (f.app (op U) s) :=
+congr_fun (germ_comp U x f) s
+
+@[simp] lemma id (x : X) (F : X.presheaf C) : stalk_map x (𝟙 F) = 𝟙 (stalk F x) :=
+(stalk_functor C x).map_id F
+
+@[simp] lemma comp (x : X) {F G H : X.presheaf C} (f : F ⟶ G) (g : G ⟶ H) :
+  stalk_map x (f ≫ g) = stalk_map x f ≫ stalk_map x g :=
+(stalk_functor C x).map_comp f g
+
+/-- An isomorphism of sheaves `F ≅ G` induces an isomorphism on the stalks -/
+def iso (x : X) {F G : X.presheaf C} (f : F ≅ G) : F.stalk x ≅ G.stalk x :=
+(stalk_functor C x).map_iso f
+
+instance is_iso (x : X) {F G : X.presheaf C} (f : F ⟶ G) [is_iso f] : is_iso (stalk_map x f) :=
+(stalk_functor C x).map_is_iso f
+
+end stalk_map
+
+open function
+
+lemma stalk_map_injective_of_app_injective {F G : presheaf (Type v) X} (f : F ⟶ G)
+  (h : ∀ U : opens X, injective (f.app (op U))) (x : X) :
+  injective (stalk_map x f) := λ s t hst,
+begin
+  rcases germ_exist F x s with ⟨U₁, hxU₁, s, rfl⟩,
+  rcases germ_exist F x t with ⟨U₂, hxU₂, t, rfl⟩,
+  rw [stalk_map.germ_comp_apply U₁ ⟨x,hxU₁⟩, stalk_map.germ_comp_apply U₂ ⟨x,hxU₂⟩] at hst,
+  obtain ⟨W, hxW, iWU₁, iWU₂, heq⟩ := G.germ_eq x hxU₁ hxU₂ _ _ hst,
+  rw [← functor_to_types.naturality, ← functor_to_types.naturality] at heq,
+  replace heq := h W heq,
+  convert congr_arg (F.germ ⟨x,hxW⟩) heq,
+  exacts [(F.germ_res_apply iWU₁ ⟨x,hxW⟩ s).symm,
+          (F.germ_res_apply iWU₂ ⟨x,hxW⟩ t).symm],
+end
+
+/-
+Note that the analogous statement for surjectivity is false: Surjectivity on stalks does not
+imply surjectivity of the components of a sheaf morphism. However it does imply that the morphism
+is an epi, but this fact is not yet formalized.
+-/
+lemma app_injective_of_stalk_maps_injective {F : sheaf (Type v) X} {G : presheaf (Type v) X}
+  (f : F.presheaf ⟶ G) (h : ∀ x : X, injective (stalk_map x f)) (U : opens X) :
+  injective (f.app (op U)) := λ s t hst,
+begin
+  apply section_ext,
+  intro x,
+  apply h x.1,
+  rw [stalk_map.germ_comp_apply, stalk_map.germ_comp_apply],
+  exact congr_arg _ hst
+end
+
+lemma app_injective_iff_stalk_maps_injective {F : sheaf (Type v) X}
+  {G : presheaf (Type v) X} (f : F.presheaf ⟶ G) :
+  (∀ x : X, injective (stalk_map x f)) ↔ (∀ U : opens X, injective (f.app (op U))) :=
+⟨app_injective_of_stalk_maps_injective f, stalk_map_injective_of_app_injective f⟩
+
+lemma app_bijective_of_stalk_maps_bijective {F G : sheaf (Type v) X} (f : F ⟶ G)
+  (h : ∀ x : X, bijective (stalk_map x f)) (U : opens X) :
+  bijective (f.app (op U)) :=
+begin
+  -- We already know that `f.app (op U)` is injective. We save that fact here as we will
+  -- need it again later.
+  have h_inj := app_injective_of_stalk_maps_injective f (λ x, (h x).1),
+  refine ⟨h_inj U, (λ t,_)⟩,
+  -- For surjectivity, we are given an arbitrary section `t` and need to find a preimage for it.
+  -- First, we show that we can find preimages *locally*. That is, for each `x : U` we construct
+  -- neighborhood `V ≤ U` and a section `s : F.obj (op V))` such that `f.app (op V) s` and `t`
+  -- agree on `V`.
+  have exists_local_preim : ∀ x : U, ∃ (V : open_nhds x.1) (iVU : V.1 ⟶ U)
+    (s : F.presheaf.obj (op V.1)), f.app (op V.1) s = G.presheaf.map iVU.op t := λ x, by {
+    -- Since `f` is surjective on stalks, we can find a preimage `s₀` of the germ of `t`
+    obtain ⟨s₀,hs₀⟩ := (h x).2 (G.presheaf.germ x t),
+    -- ... and this preimage must come from some section `s₁`
+    obtain ⟨V₁,hxV₁,s₁,hs₁⟩ := F.presheaf.germ_exist x.1 s₀,
+    subst hs₁, rename hs₀ hs₁,
+    erw stalk_map.germ_comp_apply V₁ ⟨x.1,hxV₁⟩ f s₁ at hs₁,
+    -- Now, the germ of `f.app (op V₁) s₁` equals the germ of `t`, hence they must coincide on
+    -- some open neighborhood
+    obtain ⟨V₂,hxV₂, iV₂V₁, iV₂U, heq⟩ := G.presheaf.germ_eq x.1 hxV₁ x.2 _ _ hs₁,
+    -- The restriction of `s₁` to that neighborhood is our desired local preimage
+    let s₂ := F.presheaf.map iV₂V₁.op s₁,
+    use [V₂,hxV₂,iV₂U,s₂],
+    rwa functor_to_types.naturality },
+  -- Now, we use the axiom of choice to create a function `local_preim` giving us for each point
+  -- `x : U` a neighborhood `V` and a local preimage for `t` on `V`.
+  have local_preim : Π x : U, Σ (V : open_nhds x.1) (iVU : V.1 ⟶ U),
+    {s : F.presheaf.obj (op V.1) // f.app (op V.1) s = G.presheaf.map iVU.op t } := λ x, by {
+    choose V iVU s heq using exists_local_preim x,
+    exact ⟨V,iVU,s,heq⟩ },
+  clear exists_local_preim,
+  -- In particular, we obtain a covering family of opens and a family of sections
+  let V : U → opens X := λ x, (local_preim x).1.1,
+  let sf : Π x : U, F.presheaf.obj (op (V x)) := λ x, (local_preim x).2.2.1,
+  have V_cover : U ≤ supr V := λ x hx, by {
+    rw [subtype.val_eq_coe, opens.mem_coe, opens.mem_supr],
+    exact ⟨⟨x,hx⟩,(local_preim _).1.2⟩ },
+  -- Using this data, we can glue all of the local preimages together, giving us our candidate
+  -- for the preimage of `t`
+  obtain ⟨s, s_spec, -⟩ := F.exists_unique_gluing' V U (λ x, (local_preim x).2.1) V_cover sf _,
+  use s,
+  -- Note that we generated an additional goal: We need to show that our family of sections `sf`
+  -- is actually compatible. We get that out of the way first.
+  swap,
+  { intros x y,
+    -- The only thing we know about the sections `sf` is that their image under `f` equals (the
+    -- restriction of) `t`. It is at this point that we need injectivity of `f` again!
+    apply h_inj,
+    -- Here, both sides are equal to a restriction of `t`
+    transitivity ;
+      erw [functor_to_types.naturality, (local_preim _).2.2.2, ← functor_to_types.map_comp_apply],
+    refl },
+  -- The only thing left to prove is that `s` really is a preimage of `t`
+  -- Of course, we show the equality locally
+  apply G.eq_of_locally_eq' V U (λ x, (local_preim x).2.1) V_cover,
+  intro x,
+  convert congr_arg (f.app (op (V x))) (s_spec x),
+  exacts [(functor_to_types.naturality _ _ f _ _).symm, (local_preim x).2.2.2.symm],
+end
+
+/--
+If all the stalk maps of map `f : F ⟶ G` of `Type`-valued sheaves are isomorphisms, then `f` is
+an isomorphism.
+-/
+-- Making this an instance would cause a loop in typeclass resolution with `stalk_map.is_iso`
+lemma is_iso_of_stalk_maps_iso {F G : sheaf (Type v) X} (f : F ⟶ G)
+  [∀ x : X, is_iso (stalk_map x f)] : is_iso f :=
+begin
+  -- Rather annoyingly, an isomorphism of presheaves isn't quite the same as an isomorphism of
+  -- sheaves. We have to use that the induced functor from sheaves to presheaves is fully faithful
+  haveI : is_iso ((induced_functor sheaf.presheaf).map f) :=
+  @nat_iso.is_iso_of_is_iso_app _ _ _ _ F.presheaf G.presheaf f (by {
+    intro U, op_induction U,
+    rw is_iso_iff_bijective,
+    exact app_bijective_of_stalk_maps_bijective f (λ x, (is_iso_iff_bijective _).mp (_inst_3 x)) U,
+  }),
+  exact is_iso_of_fully_faithful (induced_functor sheaf.presheaf) f,
+end
+
+/--
+A morphism of `Type`-valued sheaves `f : F ⟶ G` is an isomorphism if and only if all the stalk
+maps are isomorphisms
+-/
+lemma is_iso_iff_stalk_maps_iso {F G : sheaf (Type v) X} (f : F ⟶ G) :
+  is_iso f ↔ ∀ x : X, is_iso (stalk_map x f) :=
+begin
+  split,
+  { intros h x, resetI,
+    exact @stalk_map.is_iso _ _ _ _ x _ _ f ((induced_functor sheaf.presheaf).map_is_iso f) },
+  { intro h, resetI,
+    exact is_iso_of_stalk_maps_iso f }
+end
+
+
 end Top.presheaf