NYLL
Module

SchemeStalkDVR.lean

Nyll.EtaleFundamentalGroups.LocalGeometry.HeightOne.SchemeStalkDVR
1 declaration indexed from sourceView source ↗

Module documentation

Discrete valuation stalks at regular codimension-one points

A regular point of coheight one on an integral scheme has a discrete valuation local ring. This is the scheme-level entry point for divisorial normalization and inertia results.

Imports3
Imported by2

Declarations

theorem

isDiscreteValuationRing_stalk_of_isRegularAt_of_coheight_eq_one

L27 ↗
EtaleFundamentalGroups.isDiscreteValuationRing_stalk_of_isRegularAt_of_coheight_eq_one
Documentation

The stalk of an integral scheme at a regular codimension-one point is a discrete valuation ring.

Source context 3 commands

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

namespace EtaleFundamentalGroups
open AlgebraicGeometry Order
universe u
Lean source · statement
theorem isDiscreteValuationRing_stalk_of_isRegularAt_of_coheight_eq_one
    {X : Scheme.{u}} [IsIntegral X] (x : X)
    (hregular : X.IsRegularAt x) (hx : coheight x = 1) :
    IsDiscreteValuationRing (X.presheaf.stalk x)

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