Module

ConstantSheafDiscreteFunctions.lean

Nyll.SchemeTheory.Topology.ConstantSheafDiscreteFunctions

2 declarations indexed from sourceView source ↗

Module documentation

The actual constant sheaf as discrete-valued functions

The constant presheaf maps to the existing sheaf of continuous functions into a discrete space. This map is locally injective by evaluation and locally surjective because each continuous function is constant on the open fibre of its value at a point. Sheafification therefore gives an isomorphism from the categorical constant sheaf.

This is the constant-sheaf comparison used in the Stacks Project, tag 09ZG: https://stacks.math.columbia.edu/tag/09ZG. The Lean proof is original.

Imports3

Mathlib.CategoryTheory.Sites.ConstantSheaf
Mathlib.CategoryTheory.Sites.LocallyBijective
Mathlib.Topology.Sheaves.LocalPredicate

Imported by1

Nyll.SchemeTheory.Topology.All

def

constantToDiscreteFunctions

L37 ↗

SchemeTheory.constantToDiscreteFunctions

Documentation

Send a value to its constant function, in the existing sheaf of continuous maps into the actual discrete topological space.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopCat TopologicalSpace Opposite
namespace SchemeTheory
variable (X : TopCat.{u}) (A : Type u)

Lean source · full declaration

def constantToDiscreteFunctions :
    (Functor.const (Opens X)ᵒᵖ).obj A ⟶ presheafToTop X (TopCat.discrete.obj A) where
  app U := TypeCat.ofHom (fun a =>
    TopCat.const (X := (Opens.toTopCat X).obj U.unop) (Y := TopCat.discrete.obj A) a)
  naturality U V f := by
    apply ConcreteCategory.hom_ext
    intro a
    apply TopCat.hom_ext
    apply ContinuousMap.ext
    intro x
    rfl

def

constantSheafIsoDiscreteFunctions

L51 ↗

SchemeTheory.constantSheafIsoDiscreteFunctions