surjective_on_stalks.lean

/-
Copyright (c) 2022 Sam van Gool and Jake Levinson. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sam van Gool, Jake Levinson
-/

import topology.sheaves.presheaf
import topology.sheaves.stalks

/-!

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.

-/

universes v u

noncomputable theory

open category_theory
open topological_space
open opposite

section locally_surjective

local attribute [instance] concrete_category.has_coe_to_fun
local attribute [instance] concrete_category.has_coe_to_sort

/-- Let C be a concrete category, X a topological space. -/
variables {C : Type u} [category.{v} C] [concrete_category.{v} C] {X : Top.{v}}

/-- Let ℱ, 𝒢 : (opens X)ᵒᵖ ⥤ C be C-valued presheaves on X. -/
variables {ℱ : X.presheaf C} {𝒢 : X.presheaf C}

/-- 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 such that $T_*(s_V) = t|_V$. -/
def is_locally_surjective (T : ℱ ⟶ 𝒢) :=
  ∀ (U : opens X) (t : 𝒢.obj (op U)) (x : X) (hx : x ∈ U),
  ∃ (V : opens X) (ι : V ⟶ U) (hxV : x ∈ V) (s : ℱ.obj (op V)),
  T.app _ s = 𝒢.map ι.op t

section surjective_on_stalks

variables [category_theory.limits.has_colimits C]

/-- An equivalent condition for a map of presheaves to be locally surjective
is for all the induced maps on stalks to be surjective. -/
def is_surjective_on_stalks (T : ℱ ⟶ 𝒢) :=
  ∀ (x : X), function.surjective ((Top.presheaf.stalk_functor C x).map T)

variables [category_theory.limits.preserves_filtered_colimits (forget C)]

/-- Being locally surjective is equivalent to being surjective on stalks. -/
lemma locally_surjective_iff_surjective_on_stalks (T : ℱ ⟶ 𝒢) :
  is_locally_surjective T ↔ is_surjective_on_stalks T :=
begin
  split; intro hT,
  { /- human proof:
    Let g ∈ Γₛₜ 𝒢 x be a germ. Represent it on an open set U ⊆ X
    as ⟨t, U⟩. By local surjectivity, pass to a smaller open set V
    on which there exists s ∈ Γ_ ℱ V mapping to t |_ V.
    Then the germ of s maps to g -/

    -- Let g ∈ Γₛₜ 𝒢 x be a germ.
    intros x g,
    -- Represent it on an open set U ⊆ X as ⟨t, U⟩.
    rcases 𝒢.germ_exist x g with ⟨U, hxU, t, rfl⟩,
    -- By local surjectivity, pass to a smaller open set V
    -- on which there exists s ∈ Γ_ ℱ V mapping to t |_ V.
    rcases hT U t x hxU with ⟨V, ι, hxV, s, h_eq⟩,

    -- Then the germ of s maps to g.
    use (ℱ.germ ⟨x, hxV⟩) s,
    convert Top.presheaf.stalk_functor_map_germ_apply V ⟨x, hxV⟩ T s,

    -- New finish
    simpa [h_eq] using Top.presheaf.germ_res_apply 𝒢 ι ⟨x,hxV⟩ t,
    },

  { /- human proof:
    Let U be an open set, t ∈ Γ ℱ U a section, x ∈ U a point.
    By surjectivity on stalks, the germ of t is the image of
    some germ f ∈ Γₛₜ ℱ x. Represent f on some open set V ⊆ X as ⟨s, V⟩.
    Then there is some possibly smaller open set x ∈ W ⊆ V ∩ U on which
    we have T(s) |_ W = t |_ W. -/
    intros U t x hxU,

    set t_x := (𝒢.germ ⟨x, hxU⟩) t with ht_x,
    obtain ⟨s_x, hs_x : ((Top.presheaf.stalk_functor C x).map T) s_x = t_x⟩ := hT x t_x,
    obtain ⟨V, hxV, s, rfl⟩ := ℱ.germ_exist x s_x,
    -- rfl : ℱ.germ x s = s_x
    have key_W := 𝒢.germ_eq x hxV hxU (T.app _ s) t
      (by { convert hs_x,
            symmetry,
            convert Top.presheaf.stalk_functor_map_germ_apply _ _ _ s, }),
    obtain ⟨W, hxW, hWV, hWU, h_eq⟩ := key_W,

    refine ⟨W, hWU, hxW, ⟨ℱ.map hWV.op s, _⟩⟩,
    convert h_eq,
    simp only [← comp_apply, nat_trans.naturality] },
end

end surjective_on_stalks

end locally_surjective