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.

def TopCat.Presheaf.IsLocallySurjective {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {X : TopCat} {ℱ 𝒢 : 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 TopCat.Presheaf.isLocallySurjective_iff below.

Equations

• TopCat.Presheaf.IsLocallySurjective T = CategoryTheory.Presheaf.IsLocallySurjective (Opens.grothendieckTopology ↑X) T

theorem TopCat.Presheaf.isLocallySurjective_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {X : TopCat} {ℱ 𝒢 : Presheaf C X} (T : ℱ ⟶ 𝒢) : IsLocallySurjective T ↔ ∀ (U : TopologicalSpace.Opens ↑X) (t : CategoryTheory.ToType (𝒢.obj (Opposite.op U))), ∀ x ∈ U, ∃ (V : TopologicalSpace.Opens ↑X) (x_1 : V ≤ U), (∃ (s : CC (ℱ.obj (Opposite.op V))), (CategoryTheory.ConcreteCategory.hom (T.app (Opposite.op V))) s = restrictOpen t V x_1) ∧ x ∈ V

theorem TopCat.Presheaf.locally_surjective_iff_surjective_on_stalks {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {X : TopCat} {ℱ 𝒢 : Presheaf C X} [CategoryTheory.Limits.HasColimits C] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] (T : ℱ ⟶ 𝒢) : IsLocallySurjective T ↔ ∀ (x : ↑X), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((stalkFunctor 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.

theorem TopCat.Sheaf.isLocallySurjective_iff_epi {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Balanced (CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) C)] [(Opens.grothendieckTopology ↑X).HasSheafCompose (CategoryTheory.forget C)] [CategoryTheory.HasSheafify (Opens.grothendieckTopology ↑X) C] [(Opens.grothendieckTopology ↑X).WEqualsLocallyBijective C] [CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization C] {F G : Sheaf C X} (φ : F ⟶ G) : Presheaf.IsLocallySurjective φ.hom ↔ CategoryTheory.Epi φ