TopCat.Presheaf.locally_surjective_iff_surjective_on_stalks

theorem TopCat.Presheaf.locally_surjective_iff_surjective_on_stalks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.ConcreteCategory C] {X : TopCat} {ℱ 𝒢 : TopCat.Presheaf C X} [inst_2 : CategoryTheory.Limits.HasColimits C] [inst_3 : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] (T : ℱ ⟶ 𝒢), TopCat.Presheaf.IsLocallySurjective T ↔ ∀ (x : ↑X), Function.Surjective ⇑((TopCat.Presheaf.stalkFunctor C x).map T)

This theorem states that for a topological space `X` and a category `C` that is a concrete category and has all colimits, a morphism `T` between two `C`-valued presheaves `ℱ` and `𝒢` on `X` is locally surjective if and only if for every point `x` in `X`, the induced map on the stalks at `x` under the functor `TopCat.Presheaf.stalkFunctor` applied to `T` is a surjective function. In other words, a map between presheaves is locally surjective precisely when the maps it induces on all stalks are surjective.

More concisely: A morphism between two C-valued presheaves on a topological space X is locally surjective if and only if the induced function on stalks at every point is surjective.