Module

GenericComplementPuncture.lean

Nyll.SchemeTheory.LocalGeometry.GenericComplementPuncture

3 declarations indexed from sourceView source ↗

Module documentation

+# The stalk puncture at a generic point of an open complement

At a generic point of an irreducible component of the complement of an open subscheme, the pullback of the open to the actual stalk spectrum is exactly the puncture. This supplies the local identification used in the Noetherian induction of Stacks 0BQF. No ring Noetherianity is required.

Imports5

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

Imported by6

theorem

fromSpecStalk_preimage_open_eq_puncturedSpectrumOpen

L31 ↗

AlgebraicGeometry.Scheme.fromSpecStalk_preimage_open_eq_puncturedSpectrumOpen

Documentation

A generic point of a complement component has no other complement points among its generizations, so the stalk inverse image is 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
    {X : Scheme.{u}} (U : X.Opens)
    (x : genericPoints {z : X // z ∉ U}) :
    X.fromSpecStalk x.1.1 ⁻¹ᵁ U = puncturedSpectrumOpen (X.presheaf.stalk x.1.1)

def

genericComplementPuncturedSpectrumPullbackIso

L61 ↗

AlgebraicGeometry.Scheme.genericComplementPuncturedSpectrumPullbackIso

Documentation

The native pullback over a generic 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 genericComplementPuncturedSpectrumPullbackIso
    {X : Scheme.{u}} (U : X.Opens)
    (x : genericPoints {z : X // z ∉ U}) :
    pullback (X.fromSpecStalk x.1.1) U.ι ≅
      puncturedSpectrum (X.presheaf.stalk x.1.1)

theorem

genericComplementPuncturedSpectrumPullbackIso_hom_inclusion

L72 ↗

AlgebraicGeometry.Scheme.genericComplementPuncturedSpectrumPullbackIso_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 genericComplementPuncturedSpectrumPullbackIso_hom_inclusion
    {X : Scheme.{u}} (U : X.Opens)
    (x : genericPoints {z : X // z ∉ U}) :
    (genericComplementPuncturedSpectrumPullbackIso U x).hom ≫
        puncturedSpectrumInclusion (X.presheaf.stalk x.1.1) =
      pullback.fst (X.fromSpecStalk x.1.1) U.ι

Module documentation

Declarations

fromSpecStalk_preimage_open_eq_puncturedSpectrumOpen

genericComplementPuncturedSpectrumPullbackIso

genericComplementPuncturedSpectrumPullbackIso_hom_inclusion