LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The order function of a one-dimensional Noetherian local domain

Statement

Assume the Axiom of Choice (The Axiom of Choice), used through the finite-length suppliers in (1) and the regular-local-to-DVR supplier in (4). Let $A$ be a one-dimensional Noetherian local domain with maximal ideal $m$ and fraction field $K = Frac (A)$ (A local ring is a nonzero commutative ring with a unique maximal ideal, Left and right Noetherian rings, Krull dimension of a nonzero ring, The field of fractions $Frac (D) = (D ∖ {0})^{- 1} D$ of an integral domain). For a nonzero $A$ -module $M$ of finite length write $ℓ_{A} (M)$ for its length (Composition series and length of a module). For $0 \neq r \in K$ choose $a, b \in A ∖ {0}$ with $r = a / b$ and set ${ord}_{A} (r) : = ℓ_{A} (A / a A) - ℓ_{A} (A / b A) \in Z .$ Then:

$A / a A$ and $A / b A$ have finite length, so ${ord}_{A} (r)$ is defined. For either nonzero element $x = a$ or $b$ , if $x$ is a unit then $A / x A = 0$ has length $0$ ; otherwise $A / x A$ is Noetherian and its unique prime is $m / x A$ , so it has dimension $0$ and, by the Noetherian dimension-zero finite-length theorem (using AC), finite length.
The value ${ord}_{A} (r)$ does not depend on the presentation $r = a / b$ : if $a / b = c / d$ with $a, b, c, d \neq 0$ , then $a d = b c$ , and the two exact sequences $0 \to A / a A \overset{d}{\to} A / a d A \to A / d A \to 0$ and $0 \to A / c A \overset{b}{\to} A / b c A \to A / b A \to 0$ , together with additivity of length in short exact sequences (Module length is additive in short exact sequences), give $ℓ (A / a A) - ℓ (A / b A) = ℓ (A / c A) - ℓ (A / d A)$ .
${ord}_{A} (r s) = {ord}_{A} (r) + {ord}_{A} (s)$ and ${ord}_{A} (r^{- 1}) = - {ord}_{A} (r)$ for $r, s \in K^{*}$ ; ${ord}_{A} (r) = 0$ for $r \in A^{*}$ ; ${ord}_{A} (r) \geq 0$ for $r \in A ∖ {0}$ , with equality if and only if $r \in A^{*}$ .
If $A$ is a discrete valuation ring with normalized valuation $v_{A}$ (Discrete valuation rings), then ${ord}_{A} = v_{A}$ ; if $A$ is regular of dimension one, ${ord}_{A}$ is the normalized valuation of the discrete valuation ring $A$ (Equivalent characterizations of a DVR).

Facts & Assumptions

Given: the Axiom of Choice (The Axiom of Choice); a one-dimensional Noetherian local domain $A$ with maximal ideal $m$ and fraction field $K = Frac (A)$ ; and elements $a, b, c, d \in A ∖ {0}$ together with the quotients $A / a A$ , $A / b A$ , $A / c A$ , $A / d A$ , $A / a d A = A / b c A$ and $A / r s A$ for $r, s \in A ∖ {0}$ .

[F1]

$A$ is a local ring: it has exactly one maximal ideal, namely $m$ ; it is Noetherian; it is a domain, so its zero ideal is prime and multiplication by a nonzero element of $A$ is injective; and $\dim A = 1$ , its Krull dimension as the supremum of lengths of strict chains of prime ideals (A local ring is a nonzero commutative ring with a unique maximal ideal, Left and right Noetherian rings, Zero divisor, and integral domain: a commutative ring with $1 \neq 0$ and no zero divisors, Prime ideals and maximal ideals in a commutative ring, Krull dimension of a nonzero ring). Consequently the only prime ideals of $A$ are $(0)$ and $m$ .

[F2]

For every ideal $I \subseteq A$ , contraction along the quotient map induces an inclusion-preserving bijection $Spec (A / I) \to V (I)$ from the primes of $A / I$ to the primes of $A$ containing $I$ , inverse to $p \mapsto p / I$ (Prime ideals of a quotient ring are exactly the prime ideals containing the ideal); and $A / I$ is Noetherian (Every quotient and every localisation of a Noetherian ring is Noetherian).

[F3]

Assume AC. A commutative Noetherian ring is Artinian if and only if every prime ideal is maximal (A Noetherian ring is Artinian exactly when every prime ideal is maximal); a commutative ring is Artinian if and only if its regular module has finite length (A commutative ring is Artinian exactly when it has finite length as a module over itself, Composition series and length of a module). The submodule lattice of $A / x A$ as an $A$ -module is that of the ring $A / x A$ over itself, so the two lengths agree.

[F4]

Length is additive in short exact sequences: if $0 \to N \to M \to Q \to 0$ is exact, then $M$ has finite length if and only if $N$ and $Q$ do, and then $ℓ (M) = ℓ (N) + ℓ (Q)$ (Module length is additive in short exact sequences). By Composition series and length of a module, the zero module has length $0$ and a module of finite length $0$ is zero, so a nonzero module of finite length has length at least $1$ .

[F5]

A discrete valuation ring $V$ is the valuation ring of a discrete valuation $v$ on its fraction field, and $v : K^{\times} \to Z$ is normalized to be surjective (Discrete valuation rings); a uniformizer is an element of value $1$ . A nonzero Noetherian local ring of dimension one is regular if and only if it is a discrete valuation ring, and the one-dimensional Noetherian local domain $A$ is a discrete valuation ring if and only if it is integrally closed, equivalently a local principal ideal domain with nonzero maximal ideal (one dimensional regular local rings are dvrs, Equivalent characterizations of a DVR).

Proof

technique · direct; compute the two exact sequences and read off well-definedness, multiplicativity and the valuation comparison

1.1F1F2F3given

Finiteness and the cases $x$ unit or nonunit. Let $x \in A$ be nonzero. If $x$ is a unit, then $A / x A = 0$ , its spectrum is empty, and its length as an $A$ -module is $0$ . If $x$ is a nonunit, then $x A ⊊ A$ and $x \in m$ . A prime of $A / x A$ corresponds by [F2] to a prime of $A$ containing $x$ ; the primes of $A$ are $(0)$ and $m$ by [F1], and $x \notin (0)$ because $x \neq 0$ while $A$ is a domain. Thus the only prime of $A / x A$ is $m / x A$ , which is proper and maximal since $x A \subseteq m$ . By [F2], $A / x A$ is Noetherian; every one of its prime ideals is maximal, so it is Artinian and its regular module has finite length by [F3]. Applying these two cases to $x = a, b, c, d$ and $x y$ for nonzero $x, y$ shows that $ℓ_{A} (A / a A)$ and $ℓ_{A} (A / b A)$ , and likewise $ℓ_{A} (A / c A)$ , $ℓ_{A} (A / d A)$ and $ℓ_{A} (A / x y A)$ , are defined natural numbers.

2.1F1F4step 1.1algebra

Additivity of the length of $A / x y A$ . For $x, y \neq 0$ the sequence $0 ⟶ A / x A \overset{y}{\to} A / x y A ⟶ A / y A ⟶ 0$ is exact: multiplication by $y$ is well defined because $y (x) \subseteq (x y)$ , it is injective because $y$ is a nonzerodivisor of the domain $A$ , its image is the submodule $(y) / (x y)$ of $A / x y A$ , and the reduction $A / x y A \to A / y A$ is well defined with kernel exactly $(y) / (x y)$ . Since all three modules have finite length by step 1.1, [F4] gives $ℓ_{A} (A / x y A) = ℓ_{A} (A / x A) + ℓ_{A} (A / y A)$ .

2.2F4step 1.1algebra

Values on $A$ and units. If $r = u \in A^{\times}$ , then ${ord}_{A} (u) = ℓ_{A} (A / u A) - ℓ_{A} (A / A) = ℓ_{A} (0) - 0 = 0$ by [F4]. If $r = x \in A ∖ {0}$ , then ${ord}_{A} (x) = ℓ_{A} (A / x A) - ℓ_{A} (A / A) = ℓ_{A} (A / x A) \geq 0$ by [F4], and equality holds if and only if $ℓ_{A} (A / x A) = 0$ , if and only if $A / x A = 0$ by [F4], if and only if $x$ is a unit of $A$ .

3.1step 2.1algebra

Independence of the presentation. Suppose $a / b = c / d$ with $a, b, c, d \neq 0$ ; then $a d = b c$ by the usual fraction comparison in the domain $A$ . The sequence $0 \to A / a A \overset{d}{\to} A / a d A \to A / d A \to 0$ is exact by the argument of step 2.1, so by additivity $ℓ_{A} (A / a d A) = ℓ_{A} (A / a A) + ℓ_{A} (A / d A)$ ; likewise the sequence $0 \to A / c A \overset{b}{\to} A / b c A \to A / b A \to 0$ gives $ℓ_{A} (A / b c A) = ℓ_{A} (A / c A) + ℓ_{A} (A / b A)$ . Since $A / a d A = A / b c A$ as $a d = b c$ , subtracting the two identities yields $ℓ_{A} (A / a A) - ℓ_{A} (A / b A) = ℓ_{A} (A / c A) - ℓ_{A} (A / d A)$ . Hence ${ord}_{A} (r)$ is independent of the chosen presentation of $r$ .

3.2step 2.1algebra

Multiplicativity and inverse. Let $r = a / b$ and $s = c / d$ with $a, b, c, d \neq 0$ , so that $r s = a c / b d$ . By step 2.1, $ℓ_{A} (A / a c A) = ℓ_{A} (A / a A) + ℓ_{A} (A / c A)$ and $ℓ_{A} (A / b d A) = ℓ_{A} (A / b A) + ℓ_{A} (A / d A)$ . Therefore ${ord}_{A} (r s) = ℓ_{A} (A / a c A) - ℓ_{A} (A / b d A) = (ℓ_{A} (A / a A) - ℓ_{A} (A / b A)) + (ℓ_{A} (A / c A) - ℓ_{A} (A / d A)) = {ord}_{A} (r) + {ord}_{A} (s) .$ Applying this with $r s = 1$ and taking $r = a / b$ , $s = b / a$ gives ${ord}_{A} (r^{- 1}) = {ord}_{A} (b / a) = - {ord}_{A} (a / b) = - {ord}_{A} (r)$ .

4.1F5step 1.1algebra∎

The discrete valuation ring case. Suppose $A$ is a discrete valuation ring with normalized valuation $v_{A}$ (Discrete valuation rings). Choose a uniformizer $π$ of $A$ , an element with $v_{A} (π) = 1$ ; it exists because $v_{A}$ is normalized. Every $0 \neq x \in A$ has $v_{A} (x) = n \geq 0$ and can be written $x = u π^{n}$ with $u \in A^{\times}$ , because $x π^{- n}$ has value $0$ and is therefore a unit of $A$ . Multiplication by $u$ is an automorphism of $A$ carrying $(x)$ to $(π^{n})$ , so $A / x A ≅ A / π^{n} A$ , and the chain $A ⊋ (π) ⊋ \dots ⊋ (π^{n})$ exhibits $A / π^{n} A$ as an iterated extension of the field $A / π A$ , of length $n$ : indeed each successive quotient $(π^{i}) / (π^{i + 1})$ is isomorphic to $A / π A$ , a field, hence simple. Thus $ℓ_{A} (A / x A) = n = v_{A} (x)$ for every $0 \neq x \in A$ , and for $r = a / b$ with $a, b \neq 0$ we get ${ord}_{A} (r) = v_{A} (a) - v_{A} (b) = v_{A} (r)$ , since $v_{A}$ is a group homomorphism $K^{\times} \to Z$ and $v_{A} (b^{- 1}) = - v_{A} (b)$ . If $A$ is regular of dimension one, then the same argument applies because $A$ is a discrete valuation ring by [F5].

Depends on

Used by

Dependency tree · two levels

62 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

The Stacks Project, Chow Homology and Chern Classes, Sections 42.2-42.6 and 42.17 (order functions and the Key Lemma, tag 0EAX) (standard reference, not scraped)
Ravi Vakil, Math 245 Topics in Algebraic Geometry: Introduction to Intersection Theory, Class 2 (standard reference, not scraped)