Module

CodimensionOneBoundary.lean

Nyll.EtaleFundamentalGroups.Purity.CodimensionOneBoundary

4 declarations indexed from sourceView source ↗

Module documentation

Codimension-one points of a dense-open boundary

A point with one-dimensional stalk outside a dense open in a locally Noetherian scheme is a generic point of that open's complement. Indeed, in an affine neighbourhood, every irreducible component meets the dense open. A proper generization still outside the open would therefore give a chain of two strict generizations, contradicting the stalk dimension.

Consequently the actual pullback of the dense open to this stalk is its punctured spectrum. This supplies the generic-boundary hypothesis needed for the DVR extension step in Stacks Project, Lemma 58.31.2: https://stacks.math.columbia.edu/tag/0H2W

Neither regularity nor an assumed extension of a cover is used here.

Imports17

Nyll.SchemeTheory.LocalGeometry.GenericComplementPuncture
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Noetherian
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.Properties
Mathlib.AlgebraicGeometry.Restrict
Mathlib.AlgebraicGeometry.Stalk
Mathlib.Order.KrullDimension
Mathlib.RingTheory.KrullDimension.Basic
Mathlib.Topology.Inseparable
Mathlib.Topology.Irreducible
Mathlib.Topology.Closure
Mathlib.Topology.KrullDimension
Mathlib.Topology.Maps.Basic
Mathlib.Topology.NoetherianSpace
Mathlib.Topology.Sober
Mathlib.Tactic.NormNum

Imported by2

theorem

genericPoint_mem_dense_open

L50 ↗

AlgebraicGeometry.Scheme.genericPoint_mem_dense_open

Source context 4 commands

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

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

Lean source · statement

theorem genericPoint_mem_dense_open
    {X : Scheme.{u}} [NoetherianSpace X] (U : X.Opens)
    (hU : Dense (U : Set X)) (η : genericPoints X) : η.1 ∈ U

theorem

mem_dense_open_of_specializes_of_stalk_dimension_one

L63 ↗

AlgebraicGeometry.Scheme.mem_dense_open_of_specializes_of_stalk_dimension_one

Documentation

Every proper generization of a point with one-dimensional stalk belongs to any dense open that omits that point. The proof is affine-local, so the ambient scheme need only be locally Noetherian.

Source context 4 commands

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

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

Lean source · statement

theorem mem_dense_open_of_specializes_of_stalk_dimension_one
    {X : Scheme.{u}} [IsLocallyNoetherian X] (U : X.Opens)
    (hU : Dense (U : Set X)) (x : X)
    (hdim : ringKrullDim (X.presheaf.stalk x) = (1 : WithBot ℕ∞))
    (y : X) (hyx : y ⤳ x) (hne : y ≠ x) : y ∈ U

theorem

mem_genericPoints_complement_of_stalk_dimension_one

L121 ↗

AlgebraicGeometry.Scheme.mem_genericPoints_complement_of_stalk_dimension_one

Documentation

A codimension-one boundary point of a dense open is a generic point of an irreducible component of the complement. No regularity is required.

Source context 4 commands

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

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

Lean source · statement

theorem mem_genericPoints_complement_of_stalk_dimension_one
    {X : Scheme.{u}} [IsLocallyNoetherian X] (U : X.Opens)
    (hU : Dense (U : Set X)) (x : X) (hx : x ∉ U)
    (hdim : ringKrullDim (X.presheaf.stalk x) = (1 : WithBot ℕ∞)) :
    (⟨x, hx⟩ : {z : X // z ∉ U}) ∈ genericPoints {z : X // z ∉ U}

theorem

fromSpecStalk_preimage_dense_open_eq_puncturedSpectrumOpen

L149 ↗

AlgebraicGeometry.Scheme.fromSpecStalk_preimage_dense_open_eq_puncturedSpectrumOpen

Documentation

At every codimension-one point outside a dense open, the inverse image of that open in the actual stalk spectrum is exactly the puncture.

Source context 4 commands

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

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

Lean source · statement

theorem fromSpecStalk_preimage_dense_open_eq_puncturedSpectrumOpen
    {X : Scheme.{u}} [IsLocallyNoetherian X] (U : X.Opens)
    (hU : Dense (U : Set X)) (x : X) (hx : x ∉ U)
    (hdim : ringKrullDim (X.presheaf.stalk x) = (1 : WithBot ℕ∞)) :
    X.fromSpecStalk x ⁻¹ᵁ U = puncturedSpectrumOpen (X.presheaf.stalk x)

Module documentation

Codimension-one points of a dense-open boundary

Declarations

genericPoint_mem_dense_open

mem_dense_open_of_specializes_of_stalk_dimension_one

mem_genericPoints_complement_of_stalk_dimension_one

fromSpecStalk_preimage_dense_open_eq_puncturedSpectrumOpen