Local rings of standard-smooth relative curves

A standard-smooth algebra of relative dimension one is étale over a one-variable polynomial ring. After localizing at a prime, formal unramifiedness identifies the target maximal ideal with the image of the source maximal ideal. The source is a localization of a principal ideal domain, so the target maximal ideal is principal. The Noetherian-local-domain characterization of valuation rings then applies.

This gives the local commutative-algebra input needed to extend rational functions on a smooth curve to projective-line-valued morphisms.

theorem TauCeti.RingTheory.valuationRing_localizationAtPrime_of_isStandardSmoothOfRelativeDimension_one (K : Type u) (A : Type v) [Field K] [CommRing A] [IsDomain A] [Algebra K A] [Algebra.IsStandardSmoothOfRelativeDimension 1 K A] (q : Ideal A) [q.IsPrime] : ValuationRing (Localization.AtPrime q)

A local ring of a standard-smooth relative curve over a field is a valuation ring.

theorem TauCeti.RingTheory.valuationRing_of_isLocalizationAtPrime_of_isStandardSmoothOfRelativeDimension_one (K : Type u) (A : Type v) (Aq : Type w) [Field K] [CommRing A] [IsDomain A] [Algebra K A] [Algebra.IsStandardSmoothOfRelativeDimension 1 K A] [CommRing Aq] [IsDomain Aq] [Algebra A Aq] (q : Ideal A) [q.IsPrime] [IsLocalization.AtPrime Aq q] : ValuationRing Aq

Any chosen localization at a prime of a standard-smooth relative curve over a field is a valuation ring. This form applies directly to scheme stalks.