Module

ClosedConstantSkyscraper.lean

Nyll.SchemeTheory.Topology.ClosedConstantSkyscraper

4 declarations indexed from sourceView source ↗

Module documentation

Skyscrapers as closed-supported constant sheaves

On a space with a generic point, the skyscraper at that point is the actual sheafification of a constant presheaf. The comparison is locally bijective because every nonempty open contains the generic point. Pushing this comparison forward from the closure of a point identifies its skyscraper with the pushforward of the actual constant sheaf on that closed subset.

This supplies the closed-constant comparison in Stacks Project, tag 0CAL: https://stacks.math.columbia.edu/tag/0CAL. The Lean proof is original.

Imports6

Mathlib.CategoryTheory.Sites.ConstantSheaf
Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Mathlib.CategoryTheory.Sites.LocallyBijective
Mathlib.Topology.Sheaves.Functors
Mathlib.Topology.Sheaves.Skyscraper
Mathlib.Topology.Sober

Imported by1

Nyll.SchemeTheory.Topology.All

def

constantToSkyscraper

L42 ↗

SchemeTheory.constantToSkyscraper

Documentation

The constant presheaf maps to the skyscraper by the identity on opens containing the point, and the terminal map on the remaining opens.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopCat TopologicalSpace Opposite
namespace SchemeTheory
attribute [local instance] Classical.propDecidable
variable {X : TopCat.{u}}

Lean source · full declaration

def constantToSkyscraper (x : X) (A : Type u) :
    (Functor.const (Opens X)ᵒᵖ).obj A ⟶ skyscraperPresheaf x A where
  app U := if h : x ∈ U.unop then eqToHom (ite_eq_left h).symm
    else terminal.from A ≫ eqToHom (ite_eq_right h).symm
  naturality U V f := by
    dsimp only [Functor.const_obj_obj, skyscraperPresheaf_obj]
    by_cases hV : x ∈ V.unop
    · have hU : x ∈ U.unop := f.unop.le hV
      simp only [Functor.const_obj_map, Category.id_comp, dite_eq_left hU, dite_eq_left hV,
        skyscraperPresheaf_map]
      let eU : A = (skyscraperPresheaf x A).obj U := (ite_eq_left hU).symm
      let eUV : (skyscraperPresheaf x A).obj U =
          (skyscraperPresheaf x A).obj V := (ite_eq_left hU).trans (ite_eq_left hV).symm
      exact (eqToHom_trans eU eUV).symm
    · simp only [Functor.const_obj_map, Category.id_comp, dite_eq_right hV,
        skyscraperPresheaf_map]
      apply ((ite_eq_right hV).symm.ndrec terminalIsTerminal).hom_ext

lemma

constantToSkyscraper_app_isIso

L60 ↗

SchemeTheory.constantToSkyscraper_app_isIso

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopCat TopologicalSpace Opposite
namespace SchemeTheory
attribute [local instance] Classical.propDecidable
variable {X : TopCat.{u}}

Lean source · statement

lemma constantToSkyscraper_app_isIso (x : X) (A : Type u)
    (U : (Opens X)ᵒᵖ) (hx : x ∈ U.unop) :
    IsIso ((constantToSkyscraper x A).app U)

def

constantSheafIsoSkyscraper

L70 ↗

SchemeTheory.constantSheafIsoSkyscraper

Documentation

For a generic point, the locally bijective map from the constant presheaf induces an isomorphism of the actual constant sheaf.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopCat TopologicalSpace Opposite
namespace SchemeTheory
attribute [local instance] Classical.propDecidable
variable {X : TopCat.{u}}

Lean source · statement

def constantSheafIsoSkyscraper (x : X) (hx : ∀ y : X, x ⤳ y) (A : Type u) :
    (constantSheaf (Opens.grothendieckTopology X) (Type u)).obj A ≅
      skyscraperSheaf x A

def

closedConstantSkyscraperIso

L108 ↗

SchemeTheory.closedConstantSkyscraperIso

Documentation

A skyscraper is the pushforward of the actual constant sheaf on the closure of its point. No finiteness or separation hypothesis is needed.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopCat TopologicalSpace Opposite
namespace SchemeTheory
attribute [local instance] Classical.propDecidable
variable {X : TopCat.{u}}

Lean source · statement

def closedConstantSkyscraperIso (x : X) (A : Type u) :
    (TopCat.Sheaf.pushforward (Type u)
      (TopCat.ofHom (⟨Subtype.val, continuous_subtype_val⟩ :
        C(closure ({x} : Set X), X)))).obj
      ((constantSheaf (Opens.grothendieckTopology (closure ({x} : Set X)))
        (Type u)).obj A) ≅ skyscraperSheaf x A

Module documentation

Skyscrapers as closed-supported constant sheaves

Declarations

constantToSkyscraper

constantToSkyscraper_app_isIso

constantSheafIsoSkyscraper

closedConstantSkyscraperIso