Locally surjective maps of presheaves. #

Let X be a topological space, ℱ and 𝒢 presheaves on X, T : ℱ ⟶ 𝒢 a map.

In this file we formulate two notions for what it means for T to be locally surjective:

For each open set U, each section t : 𝒢(U) is in the image of T after passing to some open cover of U.
For each x : X, the map of stalks Tₓ : ℱₓ ⟶ 𝒢ₓ is surjective.

We prove that these are equivalent.

def Top.presheaf.is_locally_surjective {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X : Top} {ℱ 𝒢 : Top.presheaf C X} (T : ℱ ⟶ 𝒢) :

Prop

A map of presheaves T : ℱ ⟶ 𝒢 is locally surjective if for any open set U, section t over U, and x ∈ U, there exists an open set x ∈ V ⊆ U and a section s over V such that $T_*(s_V) = t|_V$ .

See is_locally_surjective_iff below.

Equations

Top.presheaf.is_locally_surjective T = category_theory.is_locally_surjective (opens.grothendieck_topology ↥X) T

source

theorem Top.presheaf.is_locally_surjective_iff {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X : Top} {ℱ 𝒢 : Top.presheaf C X} (T : ℱ ⟶ 𝒢) :

Top.presheaf.is_locally_surjective T ↔ ∀ (U : topological_space.opens ↥X) (t : ↥(𝒢.obj (opposite.op U))) (x : ↥X), x ∈ U → (∃ (V : topological_space.opens ↥X) (ι : V ⟶ U), (∃ (s : ↥(ℱ.obj (opposite.op V))), ⇑(T.app (opposite.op V)) s = Top.presheaf.restrict t ι) ∧ x ∈ V)

source

theorem Top.presheaf.locally_surjective_iff_surjective_on_stalks {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X : Top} {ℱ 𝒢 : Top.presheaf C X} [category_theory.limits.has_colimits C] [category_theory.limits.preserves_filtered_colimits (category_theory.forget C)] (T : ℱ ⟶ 𝒢) :

Top.presheaf.is_locally_surjective T ↔ ∀ (x : ↥X), function.surjective ⇑((Top.presheaf.stalk_functor C x).map T)

An equivalent condition for a map of presheaves to be locally surjective is for all the induced maps on stalks to be surjective.