A valuation subring that separates a point and is small on a prescribed ideal

Stacks 090P, in Mathlib as Subring.exists_le_valuationSubring_of_isIntegrallyClosedIn, separates a point from a subring integrally closed in a field: for R ≤ K with K a field and z ∉ R, some valuation subring V ⊇ R still misses z. Independently, Ideal.image_subset_nonunits_valuationSubring puts a prescribed proper ideal J of R inside the non-units of some valuation subring containing R. Neither gives both at once, and the valuative criterion for integrality by continuous valuations needs both of a single V: missing z is what refutes integrality, while J landing strictly below 1 is what makes the induced valuation continuous when J is an ideal of definition.

The hypothesis that combines them

Both conclusions can be read off one maximal ideal 𝔪 of R: the point is separated when 𝔪 contains every denominator of z — the s ∈ R with s * z ∈ R, which are the denominator ideal Algebra.denIdeal K z — and J lands below 1 when 𝔪 contains J. So the hypothesis the construction actually needs is that the denominators and J sit inside a common proper ideal, i.e. that their supremum is not ⊤; that is what the main theorem assumes.

The form this takes in practice is that a power of J consists of denominators. That implies the supremum hypothesis — choose 𝔪 over the denominators, and primality pulls J itself into it — so the power-based statement is a corollary, recorded here because it is the shape a topological ring hands over: multiplication by z is continuous and the powers of an ideal of definition are a neighbourhood basis of 0, so some power of it multiplies z back into any given open subring. That step is topological and is left to the caller, which is why this file states algebraic hypotheses and sits beside the Mathlib lemma it refines.

Main results

• Subring.exists_le_valuationSubring_notMem_valuation_lt_one : the combined statement, under the supremum hypothesis.
• Subring.exists_le_valuationSubring_notMem_valuation_lt_one_of_pow_mul_mem : the corollary under the power hypothesis.
• LocalSubring.isIntegrallyClosedIn_ofPrime : localising at a prime preserves integral closedness in K, which is what lets Stacks 090P part (2) apply to the local subring built in that proof.
• LocalSubring.notMem_ofPrime_of_denIdeal_le : a point whose denominators all lie in 𝔪 is still missing from the localisation at 𝔪.

References

• The Stacks Project, Tag 090P.
• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 7.18, whose proof is given there as the citation [Hu2, Lemma 3.3].

Provenance

Adapted from C. Birkbeck, AINTLIB, branch dev/adic-spaces, commit 37bbdaeb9, projects/AdicSpaces/Adic spaces/Presheaf.lean, declarations conductorIdeal, conductorIdeal_ne_top, notMem_ofPrime_of_conductor_le, isIntegrallyClosedIn_ofPrime and exists_valuationSubring_of_notMem_integralClosure, where this argument is carried out. Adapted, not copied. That development states the result for a topological ring with a pair of definition, with R the integral closure of an open subring in a fraction field, and defines its own conductorIdeal; here the statement is purely algebraic — an arbitrary subring integrally closed in K, an arbitrary ideal, and the explicit hypothesis that it generates a proper ideal together with the denominators of z — and the denominators are this repository's existing Algebra.denIdeal rather than a new definition.

theorem LocalSubring.isIntegrallyClosedIn_ofPrime {K : Type u_1} [Field K] (R : Subring K) [IsIntegrallyClosedIn (↥R) K] (𝔪 : Ideal ↥R) [𝔪.IsPrime] : IsIntegrallyClosedIn (↥(ofPrime R 𝔪).toSubring) K

Localising at a prime preserves integral closedness in K. If x : K is integral over R localised at 𝔪, clearing denominators makes m • x integral over R itself for some m ∉ 𝔪; closedness of R puts m • x in R, and m is a unit downstairs.

theorem LocalSubring.notMem_ofPrime_of_denIdeal_le {K : Type u_1} [Field K] (R : Subring K) (𝔪 : Ideal ↥R) [𝔪.IsPrime] {z : K} (hden : Algebra.denIdeal K z ≤ 𝔪) : z ∉ (ofPrime R 𝔪).toSubring

A point survives the localisation as long as all its denominators lie in 𝔪. Writing z = a / s with s ∉ 𝔪 exhibits s as a denominator of z, hence puts s in 𝔪.

theorem Subring.exists_le_valuationSubring_notMem_valuation_lt_one {K : Type u_1} [Field K] (R : Subring K) [IsIntegrallyClosedIn (↥R) K] {z : K} {J : Ideal ↥R} (hsup : Algebra.denIdeal K z ⊔ J ≠ ⊤) : ∃ (V : ValuationSubring K), R ≤ V.toSubring ∧ z ∉ V ∧ ∀ a ∈ J, V.valuation ↑a < 1

A valuation subring separating z and strictly below 1 on J. Let R be a subring of a field K, integrally closed in K, let z : K, and let J be an ideal of R which together with the denominators of z generates a proper ideal. Then a single valuation subring V ⊇ R both misses z and has valuation < 1 at every element of J.

The hypothesis is what the construction needs and no more: one maximal ideal 𝔪 above the supremum serves both halves. It forces z ∉ R, since z ∈ R makes 1 a denominator and the denominator ideal ⊤.

This refines Stacks 090P: the separation alone is Subring.exists_le_valuationSubring_of_isIntegrallyClosedIn, and the bound on J alone is Ideal.image_subset_nonunits_valuationSubring. Taking J = ⊥ recovers the former, so the strength here is that one V does both.

theorem Subring.exists_le_valuationSubring_notMem_valuation_lt_one_of_pow_mul_mem {K : Type u_1} [Field K] (R : Subring K) [IsIntegrallyClosedIn (↥R) K] {z : K} (hz : z ∉ R) {J : Ideal ↥R} {n : ℕ} (hJ : ∀ a ∈ J ^ n, ↑a * z ∈ R) : ∃ (V : ValuationSubring K), R ≤ V.toSubring ∧ z ∉ V ∧ ∀ a ∈ J, V.valuation ↑a < 1

The power form of Subring.exists_le_valuationSubring_notMem_valuation_lt_one. If a power of J consists of denominators of z ∉ R, then the denominators and J do lie in a common proper ideal: a maximal ideal above the denominators contains J ^ n, hence J.

This is the shape a topological ring supplies, with J an ideal of definition and n given by continuity of multiplication by z.