Module

FiniteModelPrincipalStalk.lean

Nyll.SchemeTheory.Topology.FiniteModelPrincipalStalk

3 declarations indexed from sourceView source ↗

Module documentation

Principal-neighborhood stalks in finite compact-open models

The germ map from a principal Alexandrov neighborhood is an isomorphism: that neighborhood is a terminal object in the opposite neighborhood category defining the actual stalk. A singleton compact-open model recovers its generating compact open at every point of that open. The Lean proofs are original.

Imports4

Mathlib.CategoryTheory.Limits.Shapes.Terminal
Mathlib.Topology.Sheaves.Alexandrov
Mathlib.Topology.Sheaves.Stalks
Nyll.SchemeTheory.Topology.CompactOpenFiniteModels

Imported by3

def

principalOpenStalkIso

L32 ↗

SchemeTheory.principalOpenStalkIso

Documentation

The actual germ map identifies sections on a principal open with the stalk of any type-valued presheaf in the upper-set topology.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopCat TopologicalSpace Topology Opposite
namespace SchemeTheory

Lean source · statement

def principalOpenStalkIso {Y : TopCat.{u}} [Preorder Y] [Topology.IsUpperSet Y]
    (P : Y.Presheaf (Type u)) (y : Y) :
    P.obj (op (Alexandrov.principalOpen y)) ≅ TopCat.Presheaf.stalk P y

theorem

principalOpenStalkIso_hom

L48 ↗

SchemeTheory.principalOpenStalkIso_hom

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopCat TopologicalSpace Topology Opposite
namespace SchemeTheory

Lean source · statement

theorem principalOpenStalkIso_hom {Y : TopCat.{u}} [Preorder Y] [Topology.IsUpperSet Y]
    (P : Y.Presheaf (Type u)) (y : Y) :
    (principalOpenStalkIso P y).hom = TopCat.Presheaf.germ P
      (Alexandrov.principalOpen y) y (Alexandrov.self_mem_principalOpen y)

theorem

neighborhood_singleton

L57 ↗

SchemeTheory.CompactOpenFiniteModel.neighborhood_singleton

Documentation

A single compact-open coordinate gives exactly that open as the principal-neighborhood preimage at each point it contains.

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
namespace CompactOpenFiniteModel

Lean source · statement

theorem neighborhood_singleton {X : TopCat.{u}} (U : CompactOpens X)
    (x : X) (hx : x ∈ (U : Set X)) : neighborhood {U} x = U.toOpens

Module documentation

Principal-neighborhood stalks in finite compact-open models

Declarations

principalOpenStalkIso

principalOpenStalkIso_hom

neighborhood_singleton