NYLL
Module

CodimensionOneGenericFiber.lean

Nyll.EtaleFundamentalGroups.Purity.CodimensionOneGenericFiber
5 declarations indexed from sourceView source ↗

Module documentation

Canonical generic maps at a codimension-one boundary point

For a dense open and a missing point whose stalk is a DVR, the actual stalk overlap is identified with the spectrum of its fraction field. The induced map from that fraction field to the open preserves the map to the ambient scheme.

When the open is enlarged without including the point, these two constructed generic maps agree after the inclusion. This comparison retains the same stalk, fraction field, and structural ring map; it is the input for transporting an original cover's generic fibre to an extension over the larger open in Stacks Project, Lemma 58.31.2 (tag 0H2W).

Imports10
Imported by2

Declarations

def

denseOpenDVRPullbackIso

L45 ↗
AlgebraicGeometry.Scheme.denseOpenDVRPullbackIso
Documentation

The actual stalk overlap of a dense open at a DVR boundary point is the spectrum of the original stalk's fraction field.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
variable {X : Scheme.{u}} [IsLocallyNoetherian X]
Lean source · statement
def denseOpenDVRPullbackIso
    (U : X.Opens) (hU : Dense (U : Set X)) (x : X) (hx : x ∉ U)
    [IsDomain (X.presheaf.stalk x)] [IsDiscreteValuationRing (X.presheaf.stalk x)]
    (hdim : ringKrullDim (X.presheaf.stalk x) = (1 : WithBot ℕ∞)) :
    Limits.pullback (X.fromSpecStalk x) U.ι ≅
      Spec (.of (FractionRing (X.presheaf.stalk x)))
theorem

denseOpenDVRPullbackIso_hom_SpecMap

L59 ↗
AlgebraicGeometry.Scheme.denseOpenDVRPullbackIso_hom_SpecMap
Documentation

The overlap comparison preserves the canonical morphism to the full stalk spectrum.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
variable {X : Scheme.{u}} [IsLocallyNoetherian X]
Lean source · statement
theorem denseOpenDVRPullbackIso_hom_SpecMap
    (U : X.Opens) (hU : Dense (U : Set X)) (x : X) (hx : x ∉ U)
    [IsDomain (X.presheaf.stalk x)] [IsDiscreteValuationRing (X.presheaf.stalk x)]
    (hdim : ringKrullDim (X.presheaf.stalk x) = (1 : WithBot ℕ∞)) :
    (denseOpenDVRPullbackIso U hU x hx hdim).hom ≫
        Spec.map (CommRingCat.ofHom
          (algebraMap (X.presheaf.stalk x) (FractionRing (X.presheaf.stalk x)))) =
      Limits.pullback.fst (X.fromSpecStalk x) U.ι
def

denseOpenDVRFractionFieldMap

L76 ↗
AlgebraicGeometry.Scheme.denseOpenDVRFractionFieldMap
Documentation

The canonical generic-point morphism into the original dense open, constructed from its actual stalk overlap.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
variable {X : Scheme.{u}} [IsLocallyNoetherian X]
Lean source · statement
def denseOpenDVRFractionFieldMap
    (U : X.Opens) (hU : Dense (U : Set X)) (x : X) (hx : x ∉ U)
    [IsDomain (X.presheaf.stalk x)] [IsDiscreteValuationRing (X.presheaf.stalk x)]
    (hdim : ringKrullDim (X.presheaf.stalk x) = (1 : WithBot ℕ∞)) :
    Spec (.of (FractionRing (X.presheaf.stalk x))) ⟶ U.toScheme
theorem

denseOpenDVRFractionFieldMap_comp_ι

L87 ↗
AlgebraicGeometry.Scheme.denseOpenDVRFractionFieldMap_comp_ι
Documentation

The constructed generic morphism is over the ambient scheme, with the original fraction-field coefficient map.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
variable {X : Scheme.{u}} [IsLocallyNoetherian X]
Lean source · statement
theorem denseOpenDVRFractionFieldMap_comp_ι
    (U : X.Opens) (hU : Dense (U : Set X)) (x : X) (hx : x ∉ U)
    [IsDomain (X.presheaf.stalk x)] [IsDiscreteValuationRing (X.presheaf.stalk x)]
    (hdim : ringKrullDim (X.presheaf.stalk x) = (1 : WithBot ℕ∞)) :
    denseOpenDVRFractionFieldMap U hU x hx hdim ≫ U.ι =
      Spec.map (CommRingCat.ofHom
        (algebraMap (X.presheaf.stalk x) (FractionRing (X.presheaf.stalk x)))) ≫
          X.fromSpecStalk x
theorem

denseOpenDVRFractionFieldMap_homOfLE

L117 ↗
AlgebraicGeometry.Scheme.denseOpenDVRFractionFieldMap_homOfLE
Documentation

Enlarging the dense open preserves the actual generic-point map after composition with the inclusion. Both maps use the same stalk fraction field.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
variable {X : Scheme.{u}} [IsLocallyNoetherian X]
Lean source · full declaration
theorem denseOpenDVRFractionFieldMap_homOfLE
    (U N : X.Opens) (hU : Dense (U : Set X)) (hUN : U ≤ N)
    (x : X) (hxN : x ∉ N)
    [IsDomain (X.presheaf.stalk x)] [IsDiscreteValuationRing (X.presheaf.stalk x)]
    (hdim : ringKrullDim (X.presheaf.stalk x) = (1 : WithBot ℕ∞)) :
    denseOpenDVRFractionFieldMap U hU x (fun hx ↦ hxN (hUN hx)) hdim ≫
        X.homOfLE hUN =
      denseOpenDVRFractionFieldMap N (Dense.mono hUN hU) x hxN hdim := by
  apply (cancel_mono N.ι).mp
  rw [Category.assoc, homOfLE_ι,
    denseOpenDVRFractionFieldMap_comp_ι, denseOpenDVRFractionFieldMap_comp_ι]

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