English
If all maps on opens are injective, then the induced stalk map is injective for all x.
Русский
Если отображения на открытых множествах инъективны, то индуцированное отображение стэла инъективно для всех x.
LaTeX
$$stalkFunctor_map_injective_of_app_injective$$
Lean4
/-- For presheaves valued in a concrete category whose forgetful functor preserves filtered colimits,
every element of the stalk is the germ of a section.
-/
theorem germ_exist (F : X.Presheaf C) (x : X) (t : ToType (stalk.{v, u} F x)) :
∃ (U : Opens X) (m : x ∈ U) (s : ToType (F.obj (op U))), F.germ _ x m s = t :=
by
obtain ⟨U, s, e⟩ := Types.jointly_surjective.{v, v} _ (isColimitOfPreserves (forget C) (colimit.isColimit _)) t
revert s e
induction U with
| op U => ?_
obtain ⟨V, m⟩ := U
intro s e
exact ⟨V, m, s, e⟩
