Module

ClosedComplementPuncture.lean

Nyll.SchemeTheory.LocalGeometry.ClosedComplementPuncture

3 declarations indexed from sourceView source ↗

Module documentation

Stalk punctures when the open complement consists of closed points

Every generization of a missing point, other than that point itself, lies in the original open. Its pullback to the actual local spectrum is therefore the punctured spectrum, without finiteness assumptions on X.

Imports5

Nyll.SchemeTheory.LocalGeometry.PuncturedSpectrum
Mathlib.AlgebraicGeometry.Stalk
Mathlib.AlgebraicGeometry.Properties
Mathlib.AlgebraicGeometry.Restrict
Mathlib.Topology.Inseparable

Imported by2

theorem

fromSpecStalk_preimage_open_eq_puncturedSpectrumOpen_of_closed_complement

L31 ↗

AlgebraicGeometry.Scheme.fromSpecStalk_preimage_open_eq_puncturedSpectrumOpen_of_closed_complement

Documentation

Closedness of every missing point identifies the actual stalk pullback of the original open with the puncture.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme

Lean source · statement

theorem fromSpecStalk_preimage_open_eq_puncturedSpectrumOpen_of_closed_complement
    {X : Scheme.{u}} (U : X.Opens)
    (hclosed : ∀ y : X, y ∉ U → IsClosed ({y} : Set X))
    (x : X) (hx : x ∉ U) :
    X.fromSpecStalk x ⁻¹ᵁ U = puncturedSpectrumOpen (X.presheaf.stalk x)

def

closedComplementPuncturedSpectrumPullbackIso

L58 ↗

AlgebraicGeometry.Scheme.closedComplementPuncturedSpectrumPullbackIso

Documentation

The native pullback over any closed complement point is the punctured actual local spectrum.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme

Lean source · statement

def closedComplementPuncturedSpectrumPullbackIso
    {X : Scheme.{u}} (U : X.Opens)
    (hclosed : ∀ y : X, y ∉ U → IsClosed ({y} : Set X))
    (x : X) (hx : x ∉ U) :
    pullback (X.fromSpecStalk x) U.ι ≅
      puncturedSpectrum (X.presheaf.stalk x)

theorem

closedComplementPuncturedSpectrumPullbackIso_hom_inclusion

L70 ↗

AlgebraicGeometry.Scheme.closedComplementPuncturedSpectrumPullbackIso_hom_inclusion

Documentation

The comparison retains the original map to the full stalk spectrum.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme

Lean source · statement

theorem closedComplementPuncturedSpectrumPullbackIso_hom_inclusion
    {X : Scheme.{u}} (U : X.Opens)
    (hclosed : ∀ y : X, y ∉ U → IsClosed ({y} : Set X))
    (x : X) (hx : x ∉ U) :
    (closedComplementPuncturedSpectrumPullbackIso U hclosed x hx).hom ≫
        puncturedSpectrumInclusion (X.presheaf.stalk x) =
      pullback.fst (X.fromSpecStalk x) U.ι

Module documentation

Stalk punctures when the open complement consists of closed points

Declarations

fromSpecStalk_preimage_open_eq_puncturedSpectrumOpen_of_closed_complement

closedComplementPuncturedSpectrumPullbackIso

closedComplementPuncturedSpectrumPullbackIso_hom_inclusion