Documentation

TauCeti.RingTheory.Huber.LocalizationTopology.Valuation

Extending a valuation to Wedhorn's topological localisation #

Roadmap Layer 3.1 attaches to a rational subset U = R(T/s) of X = Spa(A, A⁺) a coordinate ring together with its ring of integral elements, and asks for a natural homeomorphism

Spa (A_U, A_U⁺) ≃ U.

The map from left to right is built in TauCeti.AlgebraicGeometry.AdicSpace.Spa.Localization.Basic; the map in the other direction has to produce a point of an adic spectrum out of a point of U, and this file is its algebraic core, before any completion.

Mathlib's Valuation.extendToLocalization, specialised to the away submonoid in TauCeti.RingTheory.Valuation.ExtendToLocalization, already extends a valuation v with v s ≠ 0 from A to a localisation Aₛ away from s. What has to be proved is that the extension satisfies the two conditions defining a point of Spa (Aₛ, Aₛ⁺):

Both use v t ≤ v s for every numerator and v s ≠ 0. Continuity additionally requires v to be continuous and v ≤ 1 on the chosen ring of definition A₀; sub-unitness on the plus ring additionally requires v ≤ 1 on A⁺. For a point of Spa(A, A⁺), continuity and the bound on A⁺ are part of membership, while a choice A₀ ⊆ A⁺ supplies the remaining bound.

Why continuity needs a bound on the ring of definition #

The neighbourhoods of zero in Aₛ are the images of the powers Jⁿ of J = I · D, where D = A₀[t₁/s, …, tₙ/s]. That is an ideal of D, so a bound on v over Iⁿ alone says nothing about it: a general element is a D-combination of images from Iⁿ, and the D-factor has to be harmless. So isContinuous_extendToLocalization asks for v ≤ 1 on A₀, which together with v t ≤ v s puts the whole of D inside the valuation ring of the extension (PairOfDefinition.extendToLocalization_le_one_of_mem_locSubring).

That hypothesis is not automatic for a continuous valuation. Give ℚ the discrete topology: it is a Huber ring with ring of definition ℚ and ideal of definition 0, every valuation on it is continuous (Valuation.isContinuous_of_discreteTopology), and the p-adic valuation has v (1/p) > 1 with 1/p in the ring of definition.

It is not restrictive either, and that is what makes the results below usable rather than conditional. A ring of integral elements A⁺ is by definition open, so TauCeti.Huber.PairOfDefinition.exists_pairOfDefinition_ringOfDefinition_le supplies a pair of definition with A₀ ⊆ A⁺; and every point of Spa (A, A⁺) is ≤ 1 on A⁺. The choice of pair of definition is free, and this one costs nothing.

Main results #

The two headline results are assembled into a statement about adic spectra in TauCeti.AlgebraicGeometry.AdicSpace.Spa.Localization.Surjective.

What is not proved here #

Nothing about the completed localisation A⟨T/s⟩. Extending a continuous valuation from a Huber ring to its Hausdorff completion is a separate theorem, and it is not used or assumed below; every statement here concerns Aₛ with locTopology.

References #

Provenance #

The mathematics is Huber's, in the form of Wedhorn's §8.1 identification of the adic spectrum of a rational localisation with the rational subset; the Lean is written against this repository's own locTopology and locSubring API together with Mathlib's Valuation.extendToLocalization, and follows no existing formalisation. AINTLIB — the roadmap's designated prior formalisation of this material — was not consulted: no checkout of it was available in the authoring environment. Nothing is ported.

source
theorem TauCeti.Huber.PairOfDefinition.extendToLocalization_le_one_of_mem_locSubring {A : Type u_1} [CommRing A] [TopologicalSpace A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (S : Type u_3) [CommRing S] [Algebra A S] (P : PairOfDefinition A) (T : Finset A) (s : A) [IsLocalization.Away s S] {v : Valuation A Γ₀} (hs : v s ≠ 0) (hA₀ : ∀ a ∈ P.ringOfDefinition, v a ≤ 1) (hT : ∀ t ∈ T, v t ≤ v s) {x : S} (hx : x ∈ P.locSubring T s S) :
(v.extendToLocalization ⋯ S) x ≤ 1

The extension is ≤ 1 on D = A₀[t₁/s, …, tₙ/s]. D is generated by the image of the ring of definition together with the distinguished fractions, and the two hypotheses bound the extension by 1 on each family of generators; the valuation ring of the extension is a subring, so it swallows the whole of D.

source
theorem TauCeti.Huber.PairOfDefinition.extendToLocalization_lt_of_mem_locIdealImage {A : Type u_1} [CommRing A] [TopologicalSpace A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (S : Type u_3) [CommRing S] [Algebra A S] (P : PairOfDefinition A) (T : Finset A) (s : A) [IsLocalization.Away s S] {v : Valuation A Γ₀} (hs : v s ≠ 0) (hA₀ : ∀ a ∈ P.ringOfDefinition, v a ≤ 1) (hT : ∀ t ∈ T, v t ≤ v s) {γ : Γ₀} {n : ℕ} (hn : ∀ b ∈ P.idealImage n, v b < γ) {x : S} (hx : x ∈ P.locIdealImage T s S n) :
(v.extendToLocalization ⋯ S) x < γ

A bound on the n-th basic neighbourhood of zero in Aₛ. If v is smaller than γ on the image of Iⁿ, then the extension is smaller than γ on the image of Jⁿ.

The image of Jⁿ is not merely the image of Iⁿ: Jⁿ is the ideal of D spanned by that image, so its elements are D-combinations. That is why the hypotheses bounding the extension on D appear here as well.

source
theorem TauCeti.Huber.PairOfDefinition.isContinuous_extendToLocalization {A : Type u_1} [CommRing A] [TopologicalSpace A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (S : Type u_3) [CommRing S] [Algebra A S] (P : PairOfDefinition A) (T : Finset A) (s : A) [IsLocalization.Away s S] [IsTopologicalRing A] (hden : P.HasDenominatorPower T s S) {v : Valuation A Γ₀} (hv : v.IsContinuous) (hs : v s ≠ 0) (hA₀ : ∀ a ∈ P.ringOfDefinition, v a ≤ 1) (hT : ∀ t ∈ T, v t ≤ v s) :
(v.extendToLocalization ⋯ S).IsContinuous

The extension of a continuous valuation to Aₛ is continuous for Wedhorn's localisation topology, provided the valuation dominates the numerators by the denominator and is ≤ 1 on the ring of definition. The module docstring explains why the last hypothesis is needed and why it costs nothing.

source
theorem TauCeti.Huber.le_one_of_mem_adjoin_plus {A : Type u_1} [CommRing A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (S : Type u_3) [CommRing S] [Algebra A S] (T : Finset A) (s : A) [IsLocalization.Away s S] (Aplus : Subring A) {u : Valuation S Γ₀} (hplus : ∀ a ∈ Aplus, u ((algebraMap A S) a) ≤ 1) (hT : ∀ t ∈ T, u (Localization.divBy t s) ≤ 1) {x : S} (hx : x ∈ Algebra.adjoin (↥Aplus) (Set.range fun (t : ↥T) => Localization.divBy (↑t) s)) :
u x ≤ 1

A valuation on Aₛ that is ≤ 1 on the image of A⁺ and on the distinguished fractions is ≤ 1 on A⁺[t₁/s, …, tₙ/s].

The valuation is an arbitrary one on Aₛ, not necessarily an extension from A. For the extension of a valuation on A, see extendToLocalization_le_one_of_mem_integralClosure_adjoin_plus.

source
theorem TauCeti.Huber.le_one_of_mem_integralClosure_adjoin_plus {A : Type u_1} [CommRing A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (S : Type u_3) [CommRing S] [Algebra A S] (T : Finset A) (s : A) [IsLocalization.Away s S] (Aplus : Subring A) {u : Valuation S Γ₀} (hplus : ∀ a ∈ Aplus, u ((algebraMap A S) a) ≤ 1) (hT : ∀ t ∈ T, u (Localization.divBy t s) ≤ 1) {x : S} (hx : x ∈ integralClosure (↥(Algebra.adjoin (↥Aplus) (Set.range fun (t : ↥T) => Localization.divBy (↑t) s))) S) :
u x ≤ 1

A valuation on Aₛ that is ≤ 1 on the image of A⁺ and on the distinguished fractions is ≤ 1 on the plus ring of the localisation — the integral closure in Aₛ of A⁺[t₁/s, …, tₙ/s], which TauCeti.Huber.PairOfDefinition.isRingOfIntegralElements_integralClosure_adjoin_plus makes a ring of integral elements of Aₛ.

As with le_one_of_mem_adjoin_plus, the valuation is arbitrary; the extension of a valuation on A is the case extendToLocalization_le_one_of_mem_integralClosure_adjoin_plus below.

source
theorem TauCeti.Huber.extendToLocalization_le_one_of_mem_integralClosure_adjoin_plus {A : Type u_1} [CommRing A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (S : Type u_3) [CommRing S] [Algebra A S] (T : Finset A) (s : A) [IsLocalization.Away s S] (Aplus : Subring A) {v : Valuation A Γ₀} (hs : v s ≠ 0) (hplus : ∀ a ∈ Aplus, v a ≤ 1) (hT : ∀ t ∈ T, v t ≤ v s) {x : S} (hx : x ∈ (integralClosure (↥(Algebra.adjoin (↥Aplus) (Set.range fun (t : ↥T) => Localization.divBy (↑t) s))) S).toSubring) :
(v.extendToLocalization ⋯ S) x ≤ 1

The extension is ≤ 1 on the plus ring of the localisation — the integral closure in Aₛ of A⁺[t₁/s, …, tₙ/s], which TauCeti.Huber.PairOfDefinition.isRingOfIntegralElements_integralClosure_adjoin_plus makes a ring of integral elements of Aₛ.

This is le_one_of_mem_integralClosure_adjoin_plus for the extension of a valuation on A.