Module

FiniteCoverFilteredColimit.lean

Nyll.SchemeTheory.Topology.FiniteCoverFilteredColimit

6 declarations indexed from sourceView source ↗

Module documentation

Filtered colimits and sections over compact open subsets

The presheaf colimit of a filtered diagram of sheaves satisfies descent for every finite open covering. The proof uses the actual finite pairwise intersection diagram, whose limit expresses the sheaf condition.

Compactness then shows that a locally injective map from this presheaf is injective on compact opens. When compact opens form a basis and are stable under intersection, local lifts can be refined to a finite compact-open cover and glued. In particular, the categorical sheafification unit is bijective on compact opens, as in Stacks Project, tag 009F, parts (2) and (4). This supplies the section comparison used in tag 0CAI.

References: https://stacks.math.columbia.edu/tag/009F and https://stacks.math.columbia.edu/tag/0CAI. The Lean proof is original.

Imports10

Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
Mathlib.CategoryTheory.Limits.Types.Limits
Mathlib.CategoryTheory.Sites.LocallyInjective
Mathlib.CategoryTheory.Sites.LocallySurjective
Mathlib.Topology.Compactness.Compact
Mathlib.Topology.QuasiSeparated
Mathlib.Topology.Sheaves.Limits
Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Mathlib.Topology.Spectral.Prespectral

Imported by2

theorem

filteredColimit_preservesLimit_pairwise

L49 ↗

TopCat.Presheaf.filteredColimit_preservesLimit_pairwise

Documentation

A filtered presheaf colimit of sheaves preserves the limit expressing descent for any finite family of open subsets.

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.Presheaf
variable {X : TopCat.{u}} {I : Type u} [SmallCategory I] [IsFiltered I]

Lean source · statement

theorem filteredColimit_preservesLimit_pairwise
    (F : I ⥤ X.Presheaf (Type u))
    (hF : ∀ i : I, (F.obj i).IsSheaf)
    {ι : Type u} [Finite ι] (U : ι → Opens X) :
    PreservesLimit (Pairwise.diagram U).op (colimit F)

theorem

eq_of_pairwise_restrictions

L66 ↗

TopCat.Presheaf.eq_of_pairwise_restrictions

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.Presheaf
variable {X : TopCat.{u}} {I : Type u} [SmallCategory I] [IsFiltered I]

Lean source · statement

theorem eq_of_pairwise_restrictions
    (P : X.Presheaf (Type u)) {ι : Type u} (V : ι → Opens X)
    [PreservesLimit (Pairwise.diagram V).op P]
    (U : Opens X) (iVU : ∀ i : ι, V i ⟶ U) (hcover : U ≤ iSup V)
    (s t : P.obj (op U))
    (h : ∀ i : ι, P.map (iVU i).op s = P.map (iVU i).op t) : s = t

theorem

filteredColimit_app_injective_of_locallyInjective

L92 ↗

TopCat.Presheaf.filteredColimit_app_injective_of_locallyInjective

Documentation

Local injectivity becomes injectivity on a compact open for the presheaf filtered colimit of genuine topological sheaves.

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.Presheaf
variable {X : TopCat.{u}} {I : Type u} [SmallCategory I] [IsFiltered I]

Lean source · statement

theorem filteredColimit_app_injective_of_locallyInjective
    (F : I ⥤ X.Presheaf (Type u))
    (hF : ∀ i : I, (F.obj i).IsSheaf)
    {G : X.Presheaf (Type u)} (φ : colimit F ⟶ G)
    [CategoryTheory.Presheaf.IsLocallyInjective (Opens.grothendieckTopology X) φ]
    (U : Opens X) (hU : IsCompact (U : Set X)) :
    Function.Injective (φ.app (op U))

theorem

filteredColimit_toSheafify_app_injective

L122 ↗

TopCat.Presheaf.filteredColimit_toSheafify_app_injective

Documentation

Sheafification does not identify distinct sections of the presheaf filtered colimit over a compact open. The map is the categorical sheafification unit 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.Presheaf
variable {X : TopCat.{u}} {I : Type u} [SmallCategory I] [IsFiltered I]

Lean source · statement

theorem filteredColimit_toSheafify_app_injective
    (F : I ⥤ X.Presheaf (Type u))
    (hF : ∀ i : I, (F.obj i).IsSheaf)
    (U : Opens X) (hU : IsCompact (U : Set X)) :
    Function.Injective
      ((CategoryTheory.toSheafify (Opens.grothendieckTopology X) (colimit F)).app (op U))

theorem

filteredColimit_app_surjective_of_locallyBijective

L134 ↗

TopCat.Presheaf.filteredColimit_app_surjective_of_locallyBijective

Documentation

On a space with a compact-open basis and compact intersections of compact opens, local bijectivity onto a sheaf supplies all sections over compact opens from the presheaf filtered colimit.

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.Presheaf
variable {X : TopCat.{u}} {I : Type u} [SmallCategory I] [IsFiltered I]

Lean source · statement

theorem filteredColimit_app_surjective_of_locallyBijective
    [PrespectralSpace X] [QuasiSeparatedSpace X]
    (F : I ⥤ X.Presheaf (Type u))
    (hF : ∀ i : I, (F.obj i).IsSheaf)
    {G : X.Sheaf (Type u)} (φ : colimit F ⟶ G.obj)
    [CategoryTheory.Presheaf.IsLocallyInjective (Opens.grothendieckTopology X) φ]
    [CategoryTheory.Presheaf.IsLocallySurjective (Opens.grothendieckTopology X) φ]
    (U : Opens X) (hU : IsCompact (U : Set X)) :
    Function.Surjective (φ.app (op U))

theorem

filteredColimit_toSheafify_app_bijective

L219 ↗

TopCat.Presheaf.filteredColimit_toSheafify_app_bijective

Documentation

For a filtered diagram of topological sheaves on a prespectral, quasi-separated space, sheafification of its presheaf colimit leaves sections over every compact open unchanged.

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.Presheaf
variable {X : TopCat.{u}} {I : Type u} [SmallCategory I] [IsFiltered I]

Lean source · statement

theorem filteredColimit_toSheafify_app_bijective
    [PrespectralSpace X] [QuasiSeparatedSpace X]
    (F : I ⥤ X.Presheaf (Type u))
    (hF : ∀ i : I, (F.obj i).IsSheaf)
    (U : Opens X) (hU : IsCompact (U : Set X)) :
    Function.Bijective
      ((CategoryTheory.toSheafify (Opens.grothendieckTopology X) (colimit F)).app (op U))

Module documentation

Filtered colimits and sections over compact open subsets

Declarations

filteredColimit_preservesLimit_pairwise

eq_of_pairwise_restrictions

filteredColimit_app_injective_of_locallyInjective

filteredColimit_toSheafify_app_injective

filteredColimit_app_surjective_of_locallyBijective

filteredColimit_toSheafify_app_bijective