Module

FiniteModelStalkComparison.lean

Nyll.SchemeTheory.Topology.FiniteModelStalkComparison

3 declarations indexed from sourceView source ↗

Module documentation

Stalks of the actual finite-model approximation diagram

The stalk of q⁻¹q_*F is identified with sections of F on the inverse image of the finite model's principal neighborhood. The comparison uses the actual principal-open germ and the actual inverse-image stalk isomorphism, so its naturality can be checked on those germs.

The Lean constructions and proofs are original.

Imports5

Imported by2

def

stageStalkIso

L36 ↗

SchemeTheory.CompactOpenFiniteModel.stageStalkIso

Documentation

Principal-neighborhood sections identify with the actual stalk of each finite-model inverse-image/direct-image approximation.

Source context 5 commands

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

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

Lean source · statement

def stageStalkIso
    (F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u))
    (x : X) (S : Finset (CompactOpens X)) :
    (sectionDiagram F x).obj S ≅
      TopCat.Presheaf.stalk ((sheafDiagram F).obj S).obj x

def

stalkDiagramIso

L48 ↗

SchemeTheory.CompactOpenFiniteModel.stalkDiagramIso

Documentation

The stage stalk comparisons form a natural isomorphism: forgetting compact-open coordinates acts by ordinary restriction of sections.

Source context 5 commands

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

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

Lean source · statement

def stalkDiagramIso
    (F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)) (x : X) :
    sectionDiagram F x ≅ sheafDiagram F ⋙
      sheafToPresheaf (Opens.grothendieckTopology X) (Type u) ⋙
        TopCat.Presheaf.stalkFunctor (Type u) x

theorem

stageStalkIso_hom_counit

L67 ↗

SchemeTheory.CompactOpenFiniteModel.stageStalkIso_hom_counit

Documentation

The natural stage isomorphisms identify the actual counit cocone on stalks with the ordinary germ cocone of principal-neighborhood sections.

Source context 5 commands

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

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

Lean source · statement

theorem stageStalkIso_hom_counit
    (F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u))
    (x : X) (S : Finset (CompactOpens X)) :
    (stageStalkIso F x S).hom ≫
        (TopCat.Presheaf.stalkFunctor (Type u) x).map
          ((sheafCocone F).ι.app S).hom =
      (sectionCocone F x).ι.app S

Module documentation

Stalks of the actual finite-model approximation diagram

Declarations

stageStalkIso

stalkDiagramIso

stageStalkIso_hom_counit