Module

FiniteModelSheafColimit.lean

Nyll.SchemeTheory.Topology.FiniteModelSheafColimit

2 declarations indexed from sourceView source ↗

Module documentation

Every sheaf is the colimit of its actual finite-model approximations

For a prespectral space, the actual counits q⁻¹q_*F → F form a colimit cocone. On each stalk the diagram is the explicitly constructed diagram of principal-neighborhood sections. Its germ cocone is a colimit. Stalks preserve colimits and jointly detect isomorphisms, so the original sheaf cocone is a colimit as well.

This supplies the finite-model reduction used in the proof of Stacks Project, tag 09ZG: https://stacks.math.columbia.edu/tag/09ZG. The Lean constructions and proofs are original.

Imports7

Mathlib.CategoryTheory.Adjunction.Limits
Mathlib.CategoryTheory.Functor.ReflectsIso.Limits
Mathlib.CategoryTheory.Sites.Limits
Mathlib.Topology.Sheaves.Skyscraper
Nyll.SchemeTheory.Topology.FiniteModelStalkComparison
Nyll.SchemeTheory.Topology.FiniteModelStalkColimit
Nyll.SchemeTheory.Topology.FiniteModelSheafDiagram

Imported by2

def

sheafStalkCoconeIsColimit

L40 ↗

SchemeTheory.CompactOpenFiniteModel.sheafStalkCoconeIsColimit

Documentation

The actual counit cocone becomes a colimit after taking any stalk.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopologicalSpace
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}} [PrespectralSpace X]

Lean source · statement

def sheafStalkCoconeIsColimit
    (F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)) (x : X) :
    IsColimit ((sheafToPresheaf (Opens.grothendieckTopology X) (Type u) ⋙
      TopCat.Presheaf.stalkFunctor (Type u) x).mapCocone (sheafCocone F))

def

sheafCoconeIsColimit

L65 ↗

SchemeTheory.CompactOpenFiniteModel.sheafCoconeIsColimit