Module

ClosedDiscreteStalkOutside.lean

Nyll.SchemeTheory.Topology.ClosedDiscreteStalkOutside

1 declaration indexed from sourceView source ↗

Module documentation

The stalk outside a closed discrete-function support

The open complement of the support has exactly the empty function as section, even for an empty value type. Every germ at a point outside the support restricts to this section, so the actual stalk is terminal. The Lean proof is original.

Imports3

Mathlib.CategoryTheory.Limits.Types.Products
Mathlib.Topology.Sheaves.Stalks
Nyll.SchemeTheory.Topology.ClosedDiscreteSheaf

Imported by3

def

closedDiscreteStalkIsTerminal

L30 ↗

SchemeTheory.closedDiscreteStalkIsTerminal

Documentation

Outside a closed support, the actual supported discrete-function sheaf has a terminal stalk. No inhabitedness of the value type is needed.

Source context 4 commands

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

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

Lean source · statement

def closedDiscreteStalkIsTerminal {X : TopCat.{u}} (C : Set X) (hC : IsClosed C)
    (A : Type u) (x : X) (hx : x ∉ C) :
    IsTerminal (TopCat.Presheaf.stalk (closedDiscreteSheaf C A).obj x)

Module documentation

The stalk outside a closed discrete-function support

Declarations

closedDiscreteStalkIsTerminal