English
If all stalk maps are bijective, then the section map over U is bijective.
Русский
Если все карты стэков биективны, то отображение секций над U биективно.
LaTeX
$$$\forall U,\text{Bijective}((f.app(op\ U)))$ из условия, что все $(stalkFunctor\ C\ x).map f$.$$
Lean4
/-- For surjectivity, we are given an arbitrary section `t` and need to find a preimage for it.
We claim that it suffices to find preimages *locally*. That is, for each `x : U` we construct
a neighborhood `V ≤ U` and a section `s : F.obj (op V))` such that `f.app (op V) s` and `t`
agree on `V`. -/
theorem app_surjective_of_injective_of_locally_surjective {F G : Sheaf C X} (f : F ⟶ G) (U : Opens X)
(hinj : ∀ x ∈ U, Function.Injective ((stalkFunctor C x).map f.1))
(hsurj :
∀ (t x) (_ : x ∈ U),
∃ (V : Opens X) (_ : x ∈ V) (iVU : V ⟶ U) (s : ToType (F.1.obj (op V))), f.1.app (op V) s = G.1.map iVU.op t) :
Function.Surjective (f.1.app (op U)) :=
by
conv at hsurj =>
enter [t]
rw [Subtype.forall' (p := (· ∈ U))]
intro t
choose V mV iVU sf heq using hsurj t
have V_cover : U ≤ iSup V := by
intro x hxU
simp only [Opens.coe_iSup, Set.mem_iUnion, SetLike.mem_coe]
exact ⟨⟨x, hxU⟩, mV ⟨x, hxU⟩⟩
suffices IsCompatible F.val V sf by
-- Since `F` is a sheaf, we can glue all the local preimages together to get a global preimage.
obtain ⟨s, s_spec, -⟩ := F.existsUnique_gluing' V U iVU V_cover sf this
· use s
apply G.eq_of_locally_eq' V U iVU V_cover
intro x
rw [← ConcreteCategory.comp_apply, ← f.1.naturality, ConcreteCategory.comp_apply, s_spec, heq]
intro x y
apply section_ext
intro z hz
apply hinj z ((iVU x).le ((inf_le_left : V x ⊓ V y ≤ V x) hz))
dsimp only
rw [stalkFunctor_map_germ_apply, stalkFunctor_map_germ_apply]
simp_rw [← ConcreteCategory.comp_apply, f.1.naturality, ConcreteCategory.comp_apply, heq, ←
ConcreteCategory.comp_apply, ← G.1.map_comp]
rfl
