Module

FiniteModelStalkColimit.lean

Nyll.SchemeTheory.Topology.FiniteModelStalkColimit

4 declarations indexed from sourceView source ↗

Module documentation

The actual stalk colimit of finite-model principal sections

Sections over the inverse images of finite-model principal opens form an actual filtered diagram. Its germ cocone is a colimit at the actual stalk. Every germ has a compact-open representative, and equality of germs is witnessed after adding a compact-open coordinate to an existing model. The proof uses the concrete filtered-colimit criterion for types. The Lean proof is original.

Imports6

Mathlib.CategoryTheory.Filtered.Basic
Mathlib.CategoryTheory.Limits.Types.Filtered
Mathlib.Topology.Sheaves.Alexandrov
Mathlib.Topology.Sheaves.Stalks
Nyll.SchemeTheory.Topology.CompactOpenFiniteModels
Nyll.SchemeTheory.Topology.FiniteModelPrincipalStalk

Imported by3

theorem

sectionOpen_antitone

L35 ↗

SchemeTheory.CompactOpenFiniteModel.sectionOpen_antitone

Source context 5 commands

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

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

Lean source · statement

theorem sectionOpen_antitone {S T : Finset (CompactOpens X)}
    (h : S ⊆ T) (x : X) :
    (Opens.map (quotient T)).obj (Alexandrov.principalOpen (quotient T x)) ≤
      (Opens.map (quotient S)).obj (Alexandrov.principalOpen (quotient S x))

def

sectionDiagram

L44 ↗

SchemeTheory.CompactOpenFiniteModel.sectionDiagram

Documentation

Sections on actual inverse images of finite-model principal opens, with the actual restriction maps under finite-family refinement.

Source context 5 commands

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

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

Lean source · statement

def sectionDiagram
    (F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)) (x : X) :
    Finset (CompactOpens X) ⥤ Type u

def

sectionCocone

L64 ↗

SchemeTheory.CompactOpenFiniteModel.sectionCocone

Documentation

The actual germ cocone from finite-model principal sections to the stalk.

Source context 5 commands

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

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

Lean source · statement

def sectionCocone
    (F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)) (x : X) :
    Cocone (sectionDiagram F x)

def

sectionCoconeIsColimit

L87 ↗

SchemeTheory.CompactOpenFiniteModel.sectionCoconeIsColimit

Documentation

The finite-model section diagram has the actual stalk as its colimit. Surjectivity and eventual equality are proved directly from germs.

Source context 5 commands

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

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

Lean source · statement

def sectionCoconeIsColimit [PrespectralSpace X]
    (F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)) (x : X) :
    IsColimit (sectionCocone F x)

Module documentation

The actual stalk colimit of finite-model principal sections

Declarations

sectionOpen_antitone

sectionDiagram

sectionCocone

sectionCoconeIsColimit