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 sectiont : 𝒢(U)
is in the image ofT
after passing to some open cover ofU
. -
For each
x : X
, the map of stalksTₓ : ℱₓ ⟶ 𝒢ₓ
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.
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)
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.