English
A map of presheaves is locally surjective iff all stalk maps are surjective.
Русский
Отображение пшенев впрок является локально сюръективным тогда и только тогда, когда все отображения стежка сюръективны.
LaTeX
$$$ IsLocallySurjective T \\Leftrightarrow \\forall x, \\, Surjective\\; ((stalkFunctor\\; C\\ x).map\\; T)$$$
Lean4
/-- An equivalent condition for a map of presheaves to be locally surjective
is for all the induced maps on stalks to be surjective. -/
theorem locally_surjective_iff_surjective_on_stalks (T : ℱ ⟶ 𝒢) :
IsLocallySurjective T ↔ ∀ x : X, Function.Surjective ((stalkFunctor C x).map T) :=
by
constructor <;> intro hT
· /- human proof:
Let g ∈ Γₛₜ 𝒢 x be a germ. Represent it on an open set U ⊆ X
as ⟨t, U⟩. By local surjectivity, pass to a smaller open set V
on which there exists s ∈ Γ_ ℱ V mapping to t |_ V.
Then the germ of s maps to g -/
-- Let g ∈ Γₛₜ 𝒢 x be a germ.
intro x g
obtain ⟨U, hxU, t, rfl⟩ := 𝒢.germ_exist x g
rcases hT.imageSieve_mem t x hxU with
⟨V, ι, ⟨s, h_eq⟩, hxV⟩
-- Then the germ of s maps to g.
use ℱ.germ _ x hxV s
simp [h_eq, germ_res_apply]
· /- human proof:
Let U be an open set, t ∈ Γ ℱ U a section, x ∈ U a point.
By surjectivity on stalks, the germ of t is the image of
some germ f ∈ Γₛₜ ℱ x. Represent f on some open set V ⊆ X as ⟨s, V⟩.
Then there is some possibly smaller open set x ∈ W ⊆ V ∩ U on which
we have T(s) |_ W = t |_ W. -/
constructor
intro U t x hxU
set t_x := 𝒢.germ _ x hxU t with ht_x
obtain ⟨s_x, hs_x : ((stalkFunctor C x).map T) s_x = t_x⟩ := hT x t_x
obtain ⟨V, hxV, s, rfl⟩ := ℱ.germ_exist x s_x
have key_W :=
𝒢.germ_eq x hxV hxU (T.app _ s) t <| by
convert hs_x using 1
symm
convert stalkFunctor_map_germ_apply _ _ _ _ s
obtain ⟨W, hxW, hWV, hWU, h_eq⟩ := key_W
refine ⟨W, hWU, ⟨ℱ.map hWV.op s, ?_⟩, hxW⟩
convert h_eq using 1
simp only [← ConcreteCategory.comp_apply, T.naturality]
