NYLL
Module

SpecializationCofinalSections.lean

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

Module documentation

Global sections detected on a specialization-cofinal subset

Suppose every point specializes to a point of a subset Z. Equality of global sections is detected by their germs on Z. A global section of a sheaf lies in a subsheaf if its germs on Z lie in the subsheaf stalks. The latter assertion constructs local lifts near points of Z, uses specialization to cover the whole space, and glues by the monomorphism.

These are the stalk and local-lifting steps in the subsheaf reduction for Stacks Project, tag 09ZG. No identification of restriction stalks is assumed or asserted in this file.

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

Imports3
  • Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
  • Mathlib.CategoryTheory.Sites.Limits
  • Mathlib.Topology.Sheaves.Stalks
Imported by3

Declarations

theorem

globalSection_eq_of_germs_on_specialization_cofinal

L40 ↗
SchemeTheory.globalSection_eq_of_germs_on_specialization_cofinal
Documentation

Global sections are determined by their germs on a subset to which every point has a specialization.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace Topology Opposite
namespace SchemeTheory
variable {X : TopCat.{u}} {Z : Set X}
Lean source · statement
theorem globalSection_eq_of_germs_on_specialization_cofinal
    (hZ : ∀ x : X, ∃ z ∈ Z, x ⤳ z)
    (F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u))
    (s t : F.obj.obj (op (⊤ : Opens X)))
    (hst : ∀ z ∈ Z,
      TopCat.Presheaf.germ F.obj ⊤ z trivial s =
        TopCat.Presheaf.germ F.obj ⊤ z trivial t) : s = t
theorem

exists_globalSection_lift_of_germs_on_specialization_cofinal

L64 ↗
SchemeTheory.exists_globalSection_lift_of_germs_on_specialization_cofinal
Documentation

A global section has a preimage under a sheaf monomorphism whenever its germs have preimages on a specialization-cofinal subset.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace Topology Opposite
namespace SchemeTheory
variable {X : TopCat.{u}} {Z : Set X}
Lean source · statement
theorem exists_globalSection_lift_of_germs_on_specialization_cofinal
    (hZ : ∀ x : X, ∃ z ∈ Z, x ⤳ z)
    {F G : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)}
    (m : F ⟶ G) [Mono m]
    (s : G.obj.obj (op (⊤ : Opens X)))
    (hs : ∀ z ∈ Z, ∃ a : TopCat.Presheaf.stalk F.obj z,
      (TopCat.Presheaf.stalkFunctor (Type u) z).map m.hom a =
        TopCat.Presheaf.germ G.obj ⊤ z trivial s) :
    ∃ t : F.obj.obj (op (⊤ : Opens X)), m.hom.app (op ⊤) t = s

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