NYLL
Module

ClosedDiscreteSheaf.lean

Nyll.SchemeTheory.Topology.ClosedDiscreteSheaf
8 declarations indexed from sourceView source ↗

Module documentation

Stalks of discrete-valued functions on a closed support

The actual sheaf of continuous functions into a discrete value space has stalk equal to that value space, by evaluation. Constant functions give surjectivity, while open fibers give injectivity. Pushing forward from a subset preserves these stalks at points of the subset.

The constructions keep the actual evaluation and germ formulas visible for the closed-support pullback and restriction comparisons. The Lean proofs are original.

Imports5
  • Mathlib.CategoryTheory.ConcreteCategory.EpiMono
  • Mathlib.CategoryTheory.Limits.Types.Products
  • Mathlib.Topology.Sheaves.Functors
  • Mathlib.Topology.Sheaves.LocalPredicate
  • Mathlib.Topology.Sheaves.Stalks
Imported by7

Declarations

def

discreteFunctionsStalkEval

L35 ↗
SchemeTheory.discreteFunctionsStalkEval
Documentation

The actual evaluation morphism on the discrete-function sheaf's stalk.

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 discreteFunctionsStalkEval (X : TopCat.{u}) (A : Type u) (x : X) :
    TopCat.Presheaf.stalk (presheafToTop X (TopCat.discrete.obj A)) x ⟶ A
theorem

discreteFunctionsStalkEval_bijective

L41 ↗
SchemeTheory.discreteFunctionsStalkEval_bijective
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 discreteFunctionsStalkEval_bijective (X : TopCat.{u}) (A : Type u) (x : X) :
    Function.Bijective (discreteFunctionsStalkEval X A x)
def

discreteFunctionsStalkIso

L89 ↗
SchemeTheory.discreteFunctionsStalkIso
Documentation

Evaluation identifies the actual discrete-function sheaf's stalk with the value type, including when the value type is empty.

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 discreteFunctionsStalkIso (X : TopCat.{u}) (A : Type u) (x : X) :
    TopCat.Presheaf.stalk (presheafToTop X (TopCat.discrete.obj A)) x ≅ A
theorem

discreteFunctionsStalkIso_hom

L94 ↗
SchemeTheory.discreteFunctionsStalkIso_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 discreteFunctionsStalkIso_hom (X : TopCat.{u}) (A : Type u) (x : X) :
    (discreteFunctionsStalkIso X A x).hom = discreteFunctionsStalkEval X A x
theorem

discreteFunctionsStalkIso_germ

L99 ↗
SchemeTheory.discreteFunctionsStalkIso_germ
Documentation

The stalk isomorphism sends the germ of a continuous function to its value at the point.

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 discreteFunctionsStalkIso_germ (X : TopCat.{u}) (A : Type u) (x : X)
    (U : Opens X) (hx : x ∈ U)
    (s : (Opens.toTopCat X).obj U ⟶ TopCat.discrete.obj A) :
    (discreteFunctionsStalkIso X A x).hom
      (TopCat.Presheaf.germ (presheafToTop X (TopCat.discrete.obj A)) U x hx s) =
        s ⟨x, hx⟩
def

closedDiscreteSheaf

L120 ↗
SchemeTheory.closedDiscreteSheaf
Documentation

The actual pushforward of discrete-valued functions from a subset. Closedness is only needed to calculate stalks outside the subset.

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
variable {X : TopCat.{u}}
Lean source · statement
def closedDiscreteSheaf (C : Set X) (A : Type u) :
    CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)
def

closedDiscreteStalkIso

L127 ↗
SchemeTheory.closedDiscreteStalkIso
Documentation

At a point of the support, the actual pushforward stalk is the value type.

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
variable {X : TopCat.{u}}
Lean source · statement
def closedDiscreteStalkIso (C : Set X) (A : Type u) (x : C) :
    TopCat.Presheaf.stalk (closedDiscreteSheaf C A).obj x.1 ≅ A
theorem

closedDiscreteStalkIso_germ

L141 ↗
SchemeTheory.closedDiscreteStalkIso_germ
Documentation

The supported stalk comparison evaluates the represented function at the corresponding point of the subset.

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
variable {X : TopCat.{u}}
Lean source · statement
theorem closedDiscreteStalkIso_germ (C : Set X) (A : Type u) (x : C)
    (U : Opens X) (hx : x.1 ∈ U)
    (s : TopCat.of {z : C // z.1 ∈ U} ⟶ TopCat.discrete.obj A) :
    (closedDiscreteStalkIso C A x).hom
      (TopCat.Presheaf.germ (closedDiscreteSheaf C A).obj U x.1 hx s) =
        s ⟨x, hx⟩

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.