Proper ideals on rational localisations

For a point v of the rational subset R(T/s), the extension of v to the algebraic localisation at s has support containing the extension of supp v. The extended valuation is continuous for the localisation topology, so its support remains proper after passing to the separated completion A⟨T/s⟩. Consequently the ideal generated by supp v in the completed rational localisation is proper.

For a standard rational cover (R(T/t))_{t ∈ T}, this supplies the faithfulness step in Wedhorn's Corollary 8.32. Given a proper ideal J of A, choose a point of Spa(A,A⁺) whose support contains it, and choose a chart of the cover containing the point. Then J remains proper in that chart. Combined with the flatness of the chart maps and finite-product flatness, this is exactly the proper-ideal criterion for the comparison map to be faithfully flat.

Main results

• TauCeti.ValuationSpectrum.map_supp_toCompletionLoc_ne_top: a point in R(T/s) has proper extended support in A⟨T/s⟩.
• TauCeti.ValuationSpectrum.exists_map_toCompletionLoc_ne_top_of_span_eq_top: every proper ideal remains proper on some member of a standard rational cover.
• TauCeti.ValuationSpectrum.map_rationalLocalizationPiHom_ne_top_of_span_eq_top: every proper ideal remains proper under the comparison map to the product of the completed localisations.

References

• T. Wedhorn, Adic Spaces, Corollary 8.32.

Provenance

AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0), branch dev/adic-spaces at commit 37bbdaeb9ad9e3bc9f0d660feadc2779e455a91c, file projects/AdicSpaces/Adic spaces/Cor832.lean, was consulted. That file assumes a prime-lifting hypothesis for each chart; the continuous-support proof discharging properness here is independent, and no code is ported.

theorem TauCeti.ValuationSpectrum.map_supp_toCompletionLoc_ne_top {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hP : P.ringOfDefinition ≤ Aplus) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) {v : ValuationSpectrum A} (hv : v ∈ rationalSubset Aplus T s) : Ideal.map (P.toCompletionLoc T s S hden) v.supp ≠ ⊤

The support of a point in R(T/s) remains proper in A⟨T/s⟩.

Here S is an algebraic localisation at s, equipped with the topology specified by P, T, and hden. The ring of definition must lie in Aplus; membership in R(T/s) supplies continuity, the sub-unit condition v a ≤ 1 for a ∈ A⁺, and the inequalities v(t) ≤ v(s) ≠ 0 for t ∈ T.

theorem TauCeti.ValuationSpectrum.exists_map_toCompletionLoc_ne_top_of_span_eq_top {A : Type u_1} [CommRing A] [UniformSpace A] [T2Space A] [CompleteSpace A] [IsTopologicalRing A] [IsUniformAddGroup A] [Huber.IsHuberRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hplus : Huber.IsRingOfIntegralElements Aplus) (hP : P.ringOfDefinition ≤ Aplus) (T : Finset A) (S : ↥T → Type u_2) [(t : ↥T) → CommRing (S t)] [(t : ↥T) → Algebra A (S t)] [∀ (t : ↥T), IsLocalization.Away (↑t) (S t)] (hden : ∀ (t : ↥T), P.HasDenominatorPower T (↑t) (S t)) (hspan : Ideal.span ↑T = ⊤) {J : Ideal A} (hJ : J ≠ ⊤) : ∃ (t : ↥T), Ideal.map (P.toCompletionLoc T (↑t) (S t) ⋯) J ≠ ⊤

Every proper ideal remains proper on some chart of a standard rational cover.

The ring is a complete Hausdorff Huber ring, and Aplus is a ring of integral elements containing the chosen ring of definition. The condition that T generates the unit ideal makes the rational subsets R(T/t) a cover of Spa(A,A⁺); hden supplies each localisation topology. The ideal J need only be proper, with no closedness assumption. This is the faithfulness half of Wedhorn's Corollary 8.32, before finite-product flatness is combined with it.

theorem TauCeti.ValuationSpectrum.map_rationalLocalizationPiHom_ne_top_of_span_eq_top {A : Type u_1} [CommRing A] [UniformSpace A] [T2Space A] [CompleteSpace A] [IsTopologicalRing A] [IsUniformAddGroup A] [Huber.IsHuberRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hplus : Huber.IsRingOfIntegralElements Aplus) (hP : P.ringOfDefinition ≤ Aplus) (T : Finset A) (S : ↥T → Type u_2) [(t : ↥T) → CommRing (S t)] [(t : ↥T) → Algebra A (S t)] [∀ (t : ↥T), IsLocalization.Away (↑t) (S t)] (hden : ∀ (t : ↥T), P.HasDenominatorPower T (↑t) (S t)) (hspan : Ideal.span ↑T = ⊤) {J : Ideal A} (hJ : J ≠ ⊤) : Ideal.map (P.rationalLocalizationPiHom T S hden) J ≠ ⊤

A proper ideal stays proper under the comparison map for a standard rational cover. Together with flatness of the product, this is the ideal criterion for faithful flatness in Wedhorn's Corollary 8.32. No closedness assumption on the ideal is required.