The valuative criterion for integrality, by continuous valuations

TauCeti.isIntegral_of_forall_valuation_le_one tests integrality against every valuation. Wedhorn's Proposition 7.18(1) tests it against the continuous ones only, and that strengthening is what a point of Spa can actually supply.

The construction, for a domain

A valuation refuting integrality comes out of Stacks 090P and is not continuous. It is made continuous in three moves:

1. Separate and bound at once. Subring.exists_le_valuationSubring_notMem_valuation_lt_one_of_pow_mul_mem produces one valuation subring V of Frac R containing the integral closure of B, missing x, and strictly below 1 on the image of the ideal of definition. The strict bound is what continuity will consume; openness of B is what supplies its hypothesis, since multiplication by x is continuous. This move is exists_valuationSubring_of_not_isIntegral below, which is where the fraction field and the integral closure stay: moves 2 and 3 use only the three properties of V it returns.
2. Coarsen on the ring of definition. The comap of V.valuation is ≤ 1 on A₀, so the convex subgroup generated by a dominating generator's value absorbs every attained value ≥ 1 vacuously, and Valuation.restrictToConvex applies. Coarsening is what makes that value cofinal, which is what continuity needs. It has to happen on A₀, not on R: on R the value at x exceeds 1, so the absorption hypothesis of restrictToConvex is not available.
3. Extend back to R. PairOfDefinition.extendValuation carries the coarsened valuation from A₀ out to R along the dominating generator, which is topologically nilpotent. Continuity is then isContinuous_of_forall_le_of_cofinalValue, and the bounds at B and at x are restrictToConvex_mul_inv_le_one and one_lt_restrictToConvex_mul_inv.

Moves 2 and 3 together are PairOfDefinition.exists_continuous_coarsened_extension_of_valuation below. They are stated for a valuation of the ring of definition, and record how the resulting point compares with any ambient valuation extending it. Nothing in them uses the fraction field, and Spv R already hides the value group, so the convex subgroup and the extension can be built inside and never surface. The assembly is then move 1, the two pullbacks, and a case split.

The degenerate branch — every generator having value 0 — needs none of this: the comap is then already continuous, because a vanishing value is cofinal for free.

From domains to arbitrary Huber rings

The construction separates x from the integral closure of B inside Frac R, so it needs R to be a domain. The general case reduces to it modulo a prime. If x is not integral over B, then by TauCeti.isIntegral_of_forall_isPrime_map its image in R ⧸ J is not integral over the image of B for some prime J. The quotient is again a Huber ring (TauCeti.Huber.IsHuberRing.quotient), the image of B is open because the quotient map is, and every open subring of a Huber ring contains a ring of definition (TauCeti.Huber.exists_pairOfDefinition_ringOfDefinition_le). So the domain case applies in R ⧸ J, and the valuation it produces is pulled back along the quotient map, which preserves continuity (TauCeti.ValuationSpectrum.IsContinuous.comap). This is the reduction that takes TauCeti.isIntegral_of_forall_valuation_le_one from domains to arbitrary rings, carried along the quotient topology.

Main results

• TauCeti.Huber.PairOfDefinition.exists_continuous_coarsened_extension_of_valuation : coarsen a bounded valuation of a ring of definition along a dominating nonzero generator and extend it to a continuous point of the ambient Huber ring.
• TauCeti.Huber.exists_continuous_valuation_of_not_isIntegral : the refuting valuation, for any open subring of any Huber ring.
• TauCeti.Huber.isIntegral_of_forall_continuous_valuation_le_one : Wedhorn Proposition 7.18(1).

References

• 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, projects/AdicSpaces/Adic spaces/Presheaf.lean, declaration isIntegral_of_forall_continuous_valuation_le_one, where this route is carried out in one proof. Adapted, not copied: that statement carries [IsDomain], and the reduction modulo a prime has no counterpart there; its Phase A is Subring.exists_le_valuationSubring_notMem_valuation_lt_one_of_pow_mul_mem here; and its continuity step asked for domination over the whole ideal of definition and split off an empty generating set by hand, whereas isContinuous_of_forall_le_of_cofinalValue asks only for domination over a spanning set and isContinuous_of_forall_cofinalValue absorbs the degenerate branch.

Cofinality of the generator of a convex subgroup

Two plumbing steps, kept private because each is one rewrite away from an existing lemma and neither is wanted outside the construction below.

Separating a non-integral element, and packaging the result

Coarsening and extension

theorem TauCeti.Huber.PairOfDefinition.exists_continuous_coarsened_extension_of_valuation {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (P : PairOfDefinition R) {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v₀ : Valuation (↥P.ringOfDefinition) Γ₀) (hA₀le : ∀ (a : ↥P.ringOfDefinition), v₀ a ≤ 1) {s : Set ↥P.ringOfDefinition} {t₀ : ↥P.ringOfDefinition} (hS : Ideal.span s = P.idealOfDefinition) (ht₀I : t₀ ∈ P.idealOfDefinition) (hle : ∀ t ∈ s, v₀ t ≤ v₀ t₀) (hlt : v₀ t₀ < 1) (hne : v₀ t₀ ≠ 0) : ∃ (v : ValuationSpectrum R), v.IsContinuous ∧ ↑t₀ ∉ v.supp ∧ ∀ (w₀ : Valuation R Γ₀), (∀ (a : ↥P.ringOfDefinition), w₀ ↑a = v₀ a) → ∀ (y : R), y ≤ᵥ 1 ↔ w₀ y ≤ 1

A continuous coarsened extension of a bounded valuation of a ring of definition. Suppose t₀ belongs to the ideal of definition, has nonzero value strictly below 1, and dominates a spanning set of that ideal. Then convex restriction along its value and extension to the ambient ring give a continuous point of Spv R whose support does not contain t₀.

If w₀ is any valuation of R restricting to the given valuation on the ring of definition, the new point has value at most 1 exactly where w₀ does.

The construction, for a domain

Arbitrary Huber rings

theorem TauCeti.Huber.exists_continuous_valuation_of_not_isIntegral {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [IsHuberRing R] {B : Subring R} (hB : IsOpen ↑B) {x : R} (hx : ¬IsIntegral (↥B) x) : ∃ (v : ValuationSpectrum R), v.IsContinuous ∧ (∀ b ∈ B, b ≤ᵥ 1) ∧ ¬x ≤ᵥ 1

A continuous valuation refuting integrality. If x is not integral over an open subring B of a Huber ring R, some continuous valuation of R is ≤ 1 on B and > 1 at x. This is the substance of Wedhorn Proposition 7.18(1).

Modulo a prime J at which x stays non-integral over the image of B, the quotient is a Huber domain in which the image of B is open and so contains a ring of definition; the construction above applies there, and its valuation is pulled back along the quotient map.

theorem TauCeti.Huber.isIntegral_of_forall_continuous_valuation_le_one {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [IsHuberRing R] {B : Subring R} (hB : IsOpen ↑B) {x : R} (hvle : ∀ (v : ValuationSpectrum R), v.IsContinuous → (∀ b ∈ B, b ≤ᵥ 1) → x ≤ᵥ 1) : IsIntegral (↥B) x

The valuative criterion for integrality, by continuous valuations (Wedhorn Proposition 7.18(1)). If every continuous valuation of a Huber ring R that is bounded by 1 on an open subring B is bounded by 1 at x, then x is integral over B.

This strengthens TauCeti.isIntegral_of_forall_valuation_le_one, which quantifies over all valuations, by cutting the hypothesis down to the continuous ones — the only ones a point of Spa supplies.