Documentation

Mathlib.Topology.Sheaves.LocallySurjective

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:

  1. For each open set U, each section t : 𝒢(U) is in the image of T after passing to some open cover of U.

  2. For each x : X, the map of stalks Tₓ : ℱₓ ⟶ 𝒢ₓ is surjective.

We prove that these are equivalent.

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 TopCat.Presheaf.isLocallySurjective_iff below.

Instances For
    theorem TopCat.Presheaf.isLocallySurjective_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : TopCat} {ℱ : TopCat.Presheaf C X} {𝒢 : TopCat.Presheaf C X} (T : ℱ ⟶ 𝒢) :
    TopCat.Presheaf.IsLocallySurjective T ↔ ∀ (U : TopologicalSpace.Opens ↑X) (t : (CategoryTheory.forget C).obj (𝒢.obj (Opposite.op U))) (x : ↑X), x ∈ U → ∃ V ι, (∃ s, ↑(T.app (Opposite.op V)) s = TopCat.Presheaf.restrict t ι) ∧ x ∈ V

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