NYLL
Module

SpectralClosedDiscreteRestriction.lean

Nyll.SchemeTheory.Topology.SpectralClosedDiscreteRestriction
2 declarations indexed from sourceView source ↗

Module documentation

Extending discrete-valued sections on a closed support

The actual restriction of supported continuous functions is surjective on global sections under the original hypotheses of Stacks 09ZG. The proof applies the locally constant extension theorem on the closed support; the two orders of taking the intersection are exchanged by their explicit subtype coordinates.

Reference: https://stacks.math.columbia.edu/tag/09ZG. The Lean proofs are original.

Imports9
Imported by2

Declarations

theorem

closedDiscreteRestriction_top_surjective

L42 ↗
SchemeTheory.closedDiscreteRestriction_top_surjective
Documentation

The concrete restriction of supported discrete-valued functions is surjective on global sections under the original point-closure hypothesis.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopCat TopologicalSpace Topology Opposite
namespace SchemeTheory
variable {X : TopCat.{u}} [SpectralSpace X]
Lean source · statement
theorem closedDiscreteRestriction_top_surjective {Z C : Set X}
    (hZ : IsClosed Z) (hC : IsClosed C)
    (hconnected : ∀ x : X, IsConnected (Z ∩ closure ({x} : Set X))) (A : Type u) :
    Function.Surjective
      ((closedDiscreteRestriction
        (TopCat.ofHom (⟨Subtype.val, continuous_subtype_val⟩ : C(TopCat.of Z, X)))
        C A).hom.app (op (⊤ : Opens X)))
theorem

closedDiscreteSheaf_globalSections_surjective

L86 ↗
SchemeTheory.closedDiscreteSheaf_globalSections_surjective
Documentation

For a closed discrete-function support, global restriction through the actual inverse-image unit is surjective under the original hypotheses.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopCat TopologicalSpace Topology Opposite
namespace SchemeTheory
variable {X : TopCat.{u}} [SpectralSpace X]
Lean source · statement
theorem closedDiscreteSheaf_globalSections_surjective {Z C : Set X}
    (hZ : IsClosed Z) (hC : IsClosed C)
    (hconnected : ∀ x : X, IsConnected (Z ∩ closure ({x} : Set X))) (A : Type u) :
    Function.Surjective
      (((TopCat.Sheaf.pullbackPushforwardAdjunction (Type u)
        (TopCat.ofHom (⟨Subtype.val, continuous_subtype_val⟩ : C(TopCat.of Z, X)))).unit.app
          (closedDiscreteSheaf C A)).hom.app (op (⊤ : Opens X)))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.