NYLL
Module

PullbackSkyscraperClosedDiscrete.lean

Nyll.SchemeTheory.Topology.PullbackSkyscraperClosedDiscrete
6 declarations indexed from sourceView source ↗

Module documentation

Pullback of a skyscraper as discrete functions on its closed support

For an arbitrary continuous map, the inverse image of a skyscraper is the direct image of discrete-valued continuous functions on the inverse image of its closed support. The comparison is the actual adjoint of the constant-section map. Its stalks are identified on the support by germ evaluation, and both stalks are terminal away from the support.

This supplies the finite-stage closed-support comparison used in the topological proof of Stacks Project, tag 09ZG. Reference: https://stacks.math.columbia.edu/tag/09ZG. The Lean constructions and proofs are original.

Imports8
Imported by2

Declarations

def

skyscraperClosedSupportSection

L43 ↗
SchemeTheory.skyscraperClosedSupportSection
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopCat TopologicalSpace Topology Opposite
namespace SchemeTheory
attribute [local instance] Classical.propDecidable
variable {X Y : TopCat.{u}}
Lean source · statement
def skyscraperClosedSupportSection (q : X ⟶ Y) (y : Y) (A : Type u)
    (U : Opens Y) (s : (skyscraperPresheaf y A).obj (op U)) :
    TopCat.of {z : (q ⁻¹' closure ({y} : Set Y) : Set X) // q z.1 ∈ U} ⟶
      TopCat.discrete.obj A
def

skyscraperToClosedDiscretePushforward

L60 ↗
SchemeTheory.skyscraperToClosedDiscretePushforward
Documentation

The actual constant-section morphism from the skyscraper to the direct image of discrete functions on the inverse image of its closed support.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopCat TopologicalSpace Topology Opposite
namespace SchemeTheory
attribute [local instance] Classical.propDecidable
variable {X Y : TopCat.{u}}
Lean source · statement
def skyscraperToClosedDiscretePushforward (q : X ⟶ Y) (y : Y) (A : Type u) :
    skyscraperSheaf y A ⟶ (TopCat.Sheaf.pushforward (Type u) q).obj
      (closedDiscreteSheaf (q ⁻¹' closure ({y} : Set Y) : Set X) A)
def

pullbackSkyscraperToClosedDiscrete

L80 ↗
SchemeTheory.pullbackSkyscraperToClosedDiscrete
Documentation

The actual inverse-image adjoint of the constant-section morphism.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopCat TopologicalSpace Topology Opposite
namespace SchemeTheory
attribute [local instance] Classical.propDecidable
variable {X Y : TopCat.{u}}
Lean source · statement
def pullbackSkyscraperToClosedDiscrete (q : X ⟶ Y) (y : Y) (A : Type u) :
    (TopCat.Sheaf.pullback (Type u) q).obj (skyscraperSheaf y A) ⟶
      closedDiscreteSheaf (q ⁻¹' closure ({y} : Set Y) : Set X) A
theorem

pullbackSkyscraperToClosedDiscrete_stalk_onSupport

L88 ↗
SchemeTheory.pullbackSkyscraperToClosedDiscrete_stalk_onSupport
Documentation

On the closed support, the comparison carries the actual inverse-image germ to the same value in the skyscraper fiber.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopCat TopologicalSpace Topology Opposite
namespace SchemeTheory
attribute [local instance] Classical.propDecidable
variable {X Y : TopCat.{u}}
Lean source · statement
theorem pullbackSkyscraperToClosedDiscrete_stalk_onSupport
    (q : X ⟶ Y) (y : Y) (A : Type u)
    (x : (q ⁻¹' closure ({y} : Set Y) : Set X)) :
    (sheafStalkPullbackIso q (skyscraperSheaf y A) x.1).hom ≫
        (TopCat.Presheaf.stalkFunctor (Type u) x.1).map
          (pullbackSkyscraperToClosedDiscrete q y A).hom ≫
        (closedDiscreteStalkIso (q ⁻¹' closure ({y} : Set Y) : Set X) A x).hom =
      (skyscraperPresheafStalkOfSpecializes y A
        (specializes_iff_mem_closure.mpr x.2)).hom
theorem

pullbackSkyscraperToClosedDiscrete_stalk_isIso

L175 ↗
SchemeTheory.pullbackSkyscraperToClosedDiscrete_stalk_isIso
Documentation

Every stalk of the actual comparison is an isomorphism.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopCat TopologicalSpace Topology Opposite
namespace SchemeTheory
attribute [local instance] Classical.propDecidable
variable {X Y : TopCat.{u}}
Lean source · statement
theorem pullbackSkyscraperToClosedDiscrete_stalk_isIso
    (q : X ⟶ Y) (y : Y) (A : Type u) (x : X) :
    IsIso ((TopCat.Presheaf.stalkFunctor (Type u) x).map
      (pullbackSkyscraperToClosedDiscrete q y A).hom)
def

pullbackSkyscraperClosedDiscreteIso

L209 ↗
SchemeTheory.pullbackSkyscraperClosedDiscreteIso
Documentation

The inverse image of an actual skyscraper is the direct image of the discrete-function sheaf on the inverse image of its closed support.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopCat TopologicalSpace Topology Opposite
namespace SchemeTheory
attribute [local instance] Classical.propDecidable
variable {X Y : TopCat.{u}}
Lean source · statement
def pullbackSkyscraperClosedDiscreteIso (q : X ⟶ Y) (y : Y) (A : Type u) :
    (TopCat.Sheaf.pullback (Type u) q).obj (skyscraperSheaf y A) ≅
      closedDiscreteSheaf (q ⁻¹' closure ({y} : Set Y) : Set X) A

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