Module

ClosedDiscreteRestriction.lean

Nyll.SchemeTheory.Topology.ClosedDiscreteRestriction

4 declarations indexed from sourceView source ↗

Module documentation

Actual restriction of discrete functions on a closed support

Precomposition restricts continuous functions on a support to its inverse image. Its adjoint is a morphism from the actual sheaf pullback. At every point of the support it agrees with the actual stalk evaluation maps. These concrete maps supply the closed-support restriction square in the proof of Stacks Project, tag 09ZG.

Reference: https://stacks.math.columbia.edu/tag/09ZG. The Lean constructions and proofs are original.

Imports4

Mathlib.Topology.Sheaves.Functors
Mathlib.Topology.Sheaves.Stalks
Nyll.SchemeTheory.Topology.ClosedDiscreteSheaf
Nyll.SchemeTheory.Topology.SheafPullbackGerms

Imported by3

def

supportOpenPreimageMap

SchemeTheory.supportOpenPreimageMap

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 Y : TopCat.{u}}

Lean source · statement

def supportOpenPreimageMap (f : X ⟶ Y) (C : Set Y) (U : Opens Y) :
    TopCat.of {x : (f ⁻¹' C : Set X) // f x.1 ∈ U} ⟶
      TopCat.of {y : C // y.1 ∈ U}

def

closedDiscreteRestriction

SchemeTheory.closedDiscreteRestriction

Documentation

Restriction of supported continuous functions is a morphism of the actual sheaves, with codomain the direct image from the inverse-image support.

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 Y : TopCat.{u}}

Lean source · statement

def closedDiscreteRestriction (f : X ⟶ Y) (C : Set Y) (A : Type u) :
    closedDiscreteSheaf C A ⟶ (TopCat.Sheaf.pushforward (Type u) f).obj
      (closedDiscreteSheaf (f ⁻¹' C : Set X) A)

def

closedDiscretePullbackMap

SchemeTheory.closedDiscretePullbackMap

Documentation

The actual inverse-image adjoint of restriction of supported functions.

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 Y : TopCat.{u}}

Lean source · statement

def closedDiscretePullbackMap (f : X ⟶ Y) (C : Set Y) (A : Type u) :
    (TopCat.Sheaf.pullback (Type u) f).obj (closedDiscreteSheaf C A) ⟶
      closedDiscreteSheaf (f ⁻¹' C : Set X) A

theorem

closedDiscretePullbackMap_stalk_onSupport

SchemeTheory.closedDiscretePullbackMap_stalk_onSupport

Documentation

On the support the actual pullback comparison commutes with stalk evaluation, so it identifies the same value in the discrete fiber.

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 Y : TopCat.{u}}

Lean source · statement

theorem closedDiscretePullbackMap_stalk_onSupport
    (f : X ⟶ Y) (C : Set Y) (A : Type u) (x : (f ⁻¹' C : Set X)) :
    (sheafStalkPullbackIso f (closedDiscreteSheaf C A) x.1).hom ≫
        (TopCat.Presheaf.stalkFunctor (Type u) x.1).map
          (closedDiscretePullbackMap f C A).hom ≫
        (closedDiscreteStalkIso (f ⁻¹' C : Set X) A x).hom =
      (closedDiscreteStalkIso C A ⟨f x.1, x.2⟩).hom