Nyll.SchemeTheory.Topology.FilteredColimitRestriction

Module documentation

Surjective global restriction and filtered colimits

If global restriction is surjective at every stage of a filtered diagram, then it is surjective for any colimit cocone. Only the restriction domain needs to be compact, prespectral, and quasi-separated: its global-section functor preserves filtered colimits, and actual sheaf pullback preserves colimits as a left adjoint. A target section therefore comes from a stage, where it lifts; naturality of the actual adjunction unit gives the result.

The Lean proof is original.

theorem

sheafPullback_globalSections_surjective_of_isColimit

L39 ↗

SchemeTheory.sheafPullback_globalSections_surjective_of_isColimit

Documentation

Surjectivity of the actual global restriction map is stable under filtered colimits when global sections on the restriction domain preserve filtered colimits. Here that preservation follows from compactness and the prespectral, quasi-separated topology.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite
namespace SchemeTheory
variable {X Y : TopCat.{u}}

Lean source · statement

theorem sheafPullback_globalSections_surjective_of_isColimit
    [PrespectralSpace X] [QuasiSeparatedSpace X] [CompactSpace X]
    (f : X ⟶ Y) {I : Type u} [SmallCategory I] [IsFiltered I]
    (D : I ⥤ CategoryTheory.Sheaf (Opens.grothendieckTopology Y) (Type u))
    (c : Cocone D) (hc : IsColimit c)
    (hD : ∀ i : I, Function.Surjective
      (((TopCat.Sheaf.pullbackPushforwardAdjunction (Type u) f).unit.app (D.obj i)).hom.app
        (op (⊤ : Opens Y)))) :
    Function.Surjective
      (((TopCat.Sheaf.pullbackPushforwardAdjunction (Type u) f).unit.app c.pt).hom.app
        (op (⊤ : Opens Y)))

Module documentation

Surjective global restriction and filtered colimits

Declarations

sheafPullback_globalSections_surjective_of_isColimit