Module

SpecializationCofinalRestriction.lean

Nyll.SchemeTheory.Topology.SpecializationCofinalRestriction

3 declarations indexed from sourceView source ↗

Module documentation

Restriction to a specialization-cofinal image

For a continuous map whose image contains a specialization of every point, global restriction through the actual inverse-image adjunction is injective. Surjectivity of this restriction passes to subsheaves. In particular these statements apply to the closed inclusions in the subsheaf reduction of Stacks Project, tag 09ZG.

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

Imports10

Nyll.SchemeTheory.Topology.SheafPullbackGerms
Nyll.SchemeTheory.Topology.SpecializationCofinalSections
Mathlib.CategoryTheory.Functor.Flat
Mathlib.CategoryTheory.Limits.Constructions.EpiMono
Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
Mathlib.CategoryTheory.Sites.Limits
Mathlib.CategoryTheory.Sites.Pullback
Mathlib.CategoryTheory.Types.Basic
Mathlib.Topology.Sheaves.SheafCondition.Sites
Mathlib.Topology.Sheaves.Stalks

Imported by3

theorem

sheafStalkPullbackIso_hom_naturality

L42 ↗

SchemeTheory.sheafStalkPullbackIso_hom_naturality

Documentation

Naturality of the actual inverse-image stalk comparison.

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 Y : TopCat.{u}}

Lean source · statement

theorem sheafStalkPullbackIso_hom_naturality (f : X ⟶ Y)
    {F G : CategoryTheory.Sheaf (Opens.grothendieckTopology Y) (Type u)}
    (m : F ⟶ G) (x : X) :
    (TopCat.Presheaf.stalkFunctor (Type u) (f x)).map m.hom ≫
        (sheafStalkPullbackIso f G x).hom =
      (sheafStalkPullbackIso f F x).hom ≫
        (TopCat.Presheaf.stalkFunctor (Type u) x).map
          ((TopCat.Sheaf.pullback (Type u) f).map m).hom

theorem

sheafPullback_globalSections_injective

L106 ↗

SchemeTheory.sheafPullback_globalSections_injective

Documentation

A specialization-cofinal image detects global sections through the unit of the actual inverse-image adjunction.

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 Y : TopCat.{u}}

Lean source · statement

theorem sheafPullback_globalSections_injective (f : X ⟶ Y)
    (hf : ∀ y : Y, ∃ x : X, y ⤳ f x)
    (F : CategoryTheory.Sheaf (Opens.grothendieckTopology Y) (Type u)) :
    Function.Injective
      (((TopCat.Sheaf.pullbackPushforwardAdjunction (Type u) f).unit.app F).hom.app
        (op (⊤ : Opens Y)))

theorem

sheafPullback_globalSections_surjective_of_mono

L132 ↗

SchemeTheory.sheafPullback_globalSections_surjective_of_mono

Documentation

Surjectivity of global restriction passes from a sheaf to a subsheaf when the image of the continuous map is specialization-cofinal.

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 Y : TopCat.{u}}

Lean source · statement

theorem sheafPullback_globalSections_surjective_of_mono (f : X ⟶ Y)
    (hf : ∀ y : Y, ∃ x : X, y ⤳ f x)
    {F G : CategoryTheory.Sheaf (Opens.grothendieckTopology Y) (Type u)}
    (m : F ⟶ G) [Mono m]
    (hG : Function.Surjective
      (((TopCat.Sheaf.pullbackPushforwardAdjunction (Type u) f).unit.app G).hom.app
        (op (⊤ : Opens Y)))) :
    Function.Surjective
      (((TopCat.Sheaf.pullbackPushforwardAdjunction (Type u) f).unit.app F).hom.app
        (op (⊤ : Opens Y)))

Module documentation

Restriction to a specialization-cofinal image

Declarations

sheafStalkPullbackIso_hom_naturality

sheafPullback_globalSections_injective

sheafPullback_globalSections_surjective_of_mono