Module

CompactOpenSections.lean

Nyll.SchemeTheory.Topology.CompactOpenSections

2 declarations indexed from sourceView source ↗

Module documentation

Compact-open sections preserve filtered colimits

The colimit of topological sheaves is the sheafification of their presheaf colimit. Over a compact open in a prespectral, quasi-separated space, the sheafification unit is bijective. Comparing the evaluated presheaf colimit cocone with the evaluated sheafified cocone therefore proves that the actual sheaf sections functor preserves filtered colimits.

Reference: https://stacks.math.columbia.edu/tag/009F. The Lean proof is original.

Imports4

Mathlib.CategoryTheory.Limits.Preserves.Filtered
Mathlib.CategoryTheory.Sites.Limits
Mathlib.Topology.Sheaves.Limits
Nyll.SchemeTheory.Topology.FiniteCoverFilteredColimit

Imported by3

theorem

preservesColimit_sheafSections_of_isCompact

L37 ↗

TopCat.Sheaf.preservesColimit_sheafSections_of_isCompact

Documentation

Sections over a compact open preserve the colimit of any small filtered diagram of sheaves on the actual topological site.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite
namespace TopCat.Sheaf
variable {X : TopCat.{u}} [PrespectralSpace X] [QuasiSeparatedSpace X]

Lean source · statement

theorem preservesColimit_sheafSections_of_isCompact
    {I : Type u} [SmallCategory I] [IsFiltered I]
    (U : Opens X) (hU : IsCompact (U : Set X))
    (F : I ⥤ CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)) :
    PreservesColimit F
      ((sheafSections (Opens.grothendieckTopology X) (Type u)).obj (op U))

theorem

preservesFilteredColimits_sheafSections_of_isCompact

L72 ↗

TopCat.Sheaf.preservesFilteredColimits_sheafSections_of_isCompact