The valuative criterion for integrality

If every valuation of R that is bounded by 1 on a subring B is also bounded by 1 at x, then x is integral over B.

This is the hard direction of the correspondence Wedhorn records as Proposition 7.18, for which he gives only the citation [Hu2, Lemma 3.3]. It is the substantial ingredient of the comparison between two presentations of a rational subset, which Layer 3.1 of the roadmap asks for and which presentationRingEquiv currently takes as a hypothesis.

Method

The proof has two steps, and R is an arbitrary commutative ring in the statement.

For a domain the argument is by contraposition through the fraction field. If x is not integral over B then its image is outside the integral closure of B in Frac R, so Subring.exists_le_valuationSubring_of_isIntegrallyClosedIn — the Stacks project's 090P(1) — produces a valuation subring V containing that closure and missing the image of x. Pulling V.valuation back along the inclusion gives a valuation of R bounded by 1 on B but not at x, contradicting the hypothesis.

Routing through Frac R needs R to be a domain, which is a hypothesis Wedhorn's statement does not carry. It is removed by reducing modulo a prime: by TauCeti.isIntegral_of_forall_isPrime_map it is enough to be integral over the image of B in R ⧸ J for every prime J, and each R ⧸ J is a domain, so the domain case applies there. Its hypothesis is met because a valuation of R ⧸ J pulls back along Ideal.Quotient.mk J, by ValuativeRel.comap, to one of R, which the hypothesis on R bounds. So the criterion holds for R in general.

Main results

• TauCeti.isIntegral_of_forall_valuation_le_one: the criterion.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 7.18, stated there with the proof given as the citation [Hu2, Lemma 3.3].
• C. Birkbeck, AINTLIB, commit 37bbdaeb9, projects/AdicSpaces/Adic spaces/Presheaf.lean, isIntegral_of_forall_valuation_le_one — the proof route followed in the domain step. Adapted, not copied: that declaration carries an openness hypothesis its own underscore marks as unused, so the topology is dropped and the statement here is purely algebraic, which is why this file sits under RingTheory/Valuation/. It also assumes [IsDomain R], as every version of this criterion in that development does; the reduction to a prime quotient that removes the hypothesis has no counterpart there.

theorem TauCeti.isIntegral_of_forall_valuation_le_one {R : Type u_1} [CommRing R] {B : Subring R} {x : R} (hvle : ∀ (v : ValuativeRel R), (∀ b ∈ B, b ≤ᵥ 1) → x ≤ᵥ 1) : IsIntegral (↥B) x

The valuative criterion for integrality. If v x ≤ 1 for every valuation v of R satisfying v b ≤ 1 for all b ∈ B, then x is integral over B.

This is the hard direction of Wedhorn's Proposition 7.18, for an arbitrary commutative ring — the generality he states it in. The proof of the domain case goes through Frac R, and the general case is reduced to it by isIntegral_of_forall_isPrime_map, which asks only that x become integral in every prime quotient.