Regularity and valuation rings at codimension-one points

At a codimension-one point of a scheme, the local ring has Krull dimension one. If it is regular, it is a discrete valuation ring. This turns the regularity hypothesis on a curve into the valuation-ring hypothesis used to define orders of vanishing and to compare Weil and Cartier divisors.

The result combines TauCeti.IsRegularLocalRing.isDiscreteValuationRing_iff_ringKrullDim_eq_one with Mathlib's ringKrullDim_stalk_eq_coheight.

@[instance 100]

instance TauCeti.AlgebraicGeometry.CodimensionOnePoint.isDiscreteValuationRing_stalk {X : AlgebraicGeometry.Scheme} (x : CodimensionOnePoint X) [IsRegularLocalRing ↑(X.presheaf.stalk ↑x)] : IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)

The stalk at a regular codimension-one point is a discrete valuation ring.