NYLL
Module

CartierComponentStalkDVR.lean

Nyll.EtaleFundamentalGroups.LocalGeometry.HeightOne.CartierComponentStalkDVR
2 declarations indexed from sourceView source ↗

Module documentation

Discrete valuation stalks at Cartier component generic points

On a locally Noetherian scheme, the generic point of an effective Cartier divisor has codimension one. If the ambient scheme is regular along the divisor, its stalk there is a discrete valuation ring, even when the whole scheme is neither integral nor globally regular.

Regularity supplies the domain structure through the general regular-local ring theorem. The component has coheight one, so the shared one-dimensional regular-local criterion gives the DVR structure.

Imports5
Imported by7

Declarations

theorem

isDomain_stalk_componentGenericPoint

L37 ↗
EtaleFundamentalGroups.isDomain_stalk_componentGenericPoint
Documentation

The local ring at a Cartier component generic point is a domain when the ambient scheme is regular along the divisor. No global integrality of X is assumed.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory IsLocalRing
universe u
namespace EtaleFundamentalGroups
Lean source · statement
theorem isDomain_stalk_componentGenericPoint
    {X : Scheme.{u}} [IsLocallyNoetherian X]
    (D : X.EffectiveCartierDivisor) (hreg : D.1.IsAmbientRegularAlongSupport)
    (Z : Set D.1.subscheme) (hZ : Z ∈ irreducibleComponents D.1.subscheme) :
    IsDomain (X.presheaf.stalk (D.1.componentGenericPoint Z hZ))
theorem

isDiscreteValuationRing_stalk_componentGenericPoint

L49 ↗
EtaleFundamentalGroups.isDiscreteValuationRing_stalk_componentGenericPoint
Documentation

The local ring at a generic point of an effective Cartier component is a DVR under regularity along the divisor. Both its domain structure and its one-dimensional regularity are obtained from the stated geometric data.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory IsLocalRing
universe u
namespace EtaleFundamentalGroups
Lean source · full declaration
theorem isDiscreteValuationRing_stalk_componentGenericPoint
    {X : Scheme.{u}} [IsLocallyNoetherian X]
    (D : X.EffectiveCartierDivisor) (hreg : D.1.IsAmbientRegularAlongSupport)
    (Z : Set D.1.subscheme) (hZ : Z ∈ irreducibleComponents D.1.subscheme) :
    let : IsDomain (X.presheaf.stalk (D.1.componentGenericPoint Z hZ)) :=
      isDomain_stalk_componentGenericPoint D hreg Z hZ
    IsDiscreteValuationRing (X.presheaf.stalk (D.1.componentGenericPoint Z hZ)) := by
  intro hdomain
  let x : X := D.1.componentGenericPoint Z hZ
  let : IsRegularLocalRing (X.presheaf.stalk x) :=
    hreg.isRegularAt_componentGenericPoint Z hZ
  apply SchemeTheory.isDiscreteValuationRing_of_isRegularLocalRing_dimension_one
    (X.presheaf.stalk x)
  calc
    ringKrullDim (X.presheaf.stalk x) = (Order.coheight x : WithBot ℕ∞) :=
      ringKrullDim_stalk_eq_coheight x
    _ = (1 : WithBot ℕ∞) :=
      congrArg (fun n : ℕ∞ ↦ (n : WithBot ℕ∞))
        (D.2.coheight_componentGenericPoint_eq_one Z hZ)

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