English
If a morphism is injective on stalks and locally surjective, then it is surjective on sections over the base open.
Русский
Если морфизм инъективен на стэках и локально сюръективен, то он сюръективен на секциях над базовым открытым.
LaTeX
$$$\text{app_surjective_of_injective_of_locally_surjective}$$$
Lean4
theorem app_surjective_of_stalkFunctor_map_bijective {F G : Sheaf C X} (f : F ⟶ G) (U : Opens X)
(h : ∀ x ∈ U, Function.Bijective ((stalkFunctor C x).map f.1)) : Function.Surjective (f.1.app (op U)) :=
by
refine
app_surjective_of_injective_of_locally_surjective f U (And.left <| h · ·) fun t x hx =>
?_
-- Now we need to prove our initial claim: That we can find preimages of `t` locally.
-- Since `f` is surjective on stalks, we can find a preimage `s₀` of the germ of `t` at `x`
obtain ⟨s₀, hs₀⟩ :=
(h x hx).2
(G.presheaf.germ U x hx t)
-- ... and this preimage must come from some section `s₁` defined on some open neighborhood `V₁`
obtain ⟨V₁, hxV₁, s₁, hs₁⟩ := F.presheaf.germ_exist x s₀
subst hs₁; rename' hs₀ => hs₁
rw [stalkFunctor_map_germ_apply V₁ x hxV₁ f.1 s₁] at hs₁
obtain ⟨V₂, hxV₂, iV₂V₁, iV₂U, heq⟩ := G.presheaf.germ_eq x hxV₁ hx _ _ hs₁
use V₂, hxV₂, iV₂U, F.1.map iV₂V₁.op s₁
rw [← ConcreteCategory.comp_apply, f.1.naturality, ConcreteCategory.comp_apply, heq]
