Module

SpectralClosedSheafRestriction.lean

Nyll.SchemeTheory.Topology.SpectralClosedSheafRestriction

1 declaration indexed from sourceView source ↗

Module documentation

Global sections restrict bijectively along the spectral closed subset

Let Z be closed in a spectral space X, and suppose every point closure meets Z in a connected nonempty set. The actual inverse-image unit gives a bijection from sections of any sheaf on X to its sections on Z.

The proof uses the actual filtered colimit of finite-model approximations. Each approximation embeds in a finite product of pulled-back skyscrapers, which are actual discrete-function sheaves on closed supports. The closed support extension theorem supplies surjectivity for these factors; finite products, subobjects, and filtered colimits transfer it to the given sheaf. Specialization-cofinality gives injectivity directly.

Reference: Stacks Project, tag 09ZG, https://stacks.math.columbia.edu/tag/09ZG. The Lean proof is original.

Imports14

Imported by2

theorem

sheaf_globalSections_restriction_bijective

L52 ↗

SchemeTheory.sheaf_globalSections_restriction_bijective

Documentation

Under the original spectral, closed, and connected point-closure hypotheses, the actual sheaf restriction map on global sections is bijective.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopologicalSpace Topology Opposite
namespace SchemeTheory

Lean source · statement

theorem sheaf_globalSections_restriction_bijective
    {X : TopCat.{u}} [SpectralSpace X] {Z : Set X} (hZ : IsClosed Z)
    (hconnected : ∀ x : X, IsConnected (Z ∩ closure ({x} : Set X)))
    (F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)) :
    Function.Bijective
      (((TopCat.Sheaf.pullbackPushforwardAdjunction (Type u)
        (TopCat.ofHom
          (⟨Subtype.val, continuous_subtype_val⟩ : C(TopCat.of Z, X)))).unit.app F).hom.app
        (op (⊤ : Opens X)))

Module documentation

Global sections restrict bijectively along the spectral closed subset

Declarations

sheaf_globalSections_restriction_bijective