Documentation

TauCeti.RingTheory.Huber.Continuous.ValuativeCriterion

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 exists_continuous_valuation_of_forall_le below. They are stated there for an arbitrary valuation of R, not for the pullback of V: 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 #

References #

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 #

The construction, for a domain #

Arbitrary Huber rings #

source
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.

source
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.