Vanishing of the order of vanishing

For a Noetherian domain R of Krull dimension at most one with fraction field K, Mathlib's Ring.ordFrac R : K →*₀ ℤᵐ⁰ extends the order of vanishing Ring.ord R x = length (R ⧸ (x)) to the fraction field. This file records that the order of a nonzero element of R is trivial exactly when that element is a unit: R ⧸ (x) is the zero ring exactly when (x) is the unit ideal. Mathlib has the forward direction, Ring.ordFrac_of_isUnit; the converse is what reads "f has order zero at a codimension-one point" as "f is a unit at that point".

Main results

• TauCeti.Ring.ord_eq_zero_iff: Ring.ord R x = 0 exactly when x is a unit;
• TauCeti.Ring.isUnit_iff_ordFrac_one: x is a unit exactly when Ring.ordFrac R x = 1; this extends Mathlib's Ring.isUnit_iff_ordFrac_one_of_isDiscreteValuationRing to Noetherian domains of dimension at most one.

theorem TauCeti.Ring.ord_eq_zero_iff {R : Type u_1} [CommRing R] (x : R) : Ring.ord R x = 0 ↔ IsUnit x

The order of vanishing of a ring element is zero exactly when the element is a unit: the quotient R ⧸ (x) is trivial exactly when (x) is the unit ideal.

theorem TauCeti.Ring.isUnit_iff_ordFrac_one {R : Type u_1} [CommRing R] [IsDomain R] [IsNoetherianRing R] [Ring.KrullDimLE 1 R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {x : R} : IsUnit x ↔ (Ring.ordFrac R) ((algebraMap R K) x) = 1

In a Noetherian domain of dimension at most one, an element is a unit exactly when its order of vanishing in the fraction field is trivial. This extends Mathlib's Ring.isUnit_iff_ordFrac_one_of_isDiscreteValuationRing from discrete valuation rings to the local rings at the codimension-one points of an arbitrary locally Noetherian integral scheme.