Documentation

TauCeti.AlgebraicGeometry.AdicSpace.Cont.OfIdeal

Continuous points in Spv (A, I): Wedhorn's Theorem 7.10 and Corollary 7.12 #

Wedhorn, Adic Spaces (arXiv:1910.05934v1), Theorem 7.10 and Corollary 7.12.

Theorem 7.10 identifies Cont A inside Spv (A, IA) for a pair of definition (A₀, I), as the locus where additionally v(a) < 1 for every a ∈ I. This file proves the two conjuncts of the inclusion — a continuous point lies in Spv (A, IA), and it is sub-unit on the ideal of definition — then the converse, and assembles the identification cont_eq_spvOfIdeal_inter_setOfPred_forall_vlt_one. Corollary 7.12 follows: the sub-unit condition is closed in Spv A, so Cont A is a closed subset of the subspace Spv (A, IA).

For the inclusion, the argument needs no estimate and no pair of definition either. Membership in Spv (A, I) is cΓ_v(I) = Γ_v, which by Lemma 7.4 follows from cofinality of v at every element of a spanning set; and continuity turns topological nilpotence into cofinality. So the hypothesis that carries the proof is exactly "spanned by topologically nilpotent elements", which is what mem_spvOfIdeal_of_span_of_isTopologicallyNilpotent_of_isContinuous below assumes — and of an ideal with the same radical as I, since cΓ_v(I) sees I only through its radical. The extended ideal of a pair of definition is the case at hand, since the image of I spans IA and its elements are topologically nilpotent.

Passing through a spanning set is essential, not a convenience. A general element of IA is a sum Σ xᵢ aᵢ with xᵢ ∈ I and aᵢ ∈ A arbitrary, and such a sum need not be topologically nilpotent — the nilpotence is a property of the generators, not of the ideal they generate.

Main results #

References #

source
theorem TauCeti.ValuationSpectrum.mem_spvOfIdeal_of_span_of_isTopologicallyNilpotent_of_isContinuous {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {I J : Ideal A} (hfg : ∃ (K : Ideal A), K.FG ∧ I.radical = K.radical) {T : Set A} (hspan : Ideal.span T = J) (hrad : I.radical = J.radical) (hnil : ∀ t ∈ T, IsTopologicallyNilpotent t) {v : ValuationSpectrum A} (hv : v.IsContinuous) :
v ∈ spvOfIdeal I hfg

A continuous point lies in Spv (A, I) when some ideal with the same radical is spanned by topologically nilpotent elements. This is the membership conjunct of the inclusion half of Wedhorn Theorem 7.10: continuity makes the value at a topologically nilpotent element cofinal, and Lemma 7.4 only ever asks for cofinality on a spanning set.

cΓ_v(I) depends on I only through its radical, so the spanning set need not generate I itself — any J with I.radical = J.radical will do. The spanning set is not assumed finite and no pair of definition appears; both enter only in the specialisation below.

source
theorem TauCeti.ValuationSpectrum.mem_spvOfIdeal_extendedIdealOfDefinition_of_isContinuous {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) {v : ValuationSpectrum A} (hv : v.IsContinuous) :
v ∈ spvOfIdeal P.extendedIdealOfDefinition ⋯

Wedhorn Theorem 7.10, the inclusion Cont A ⊆ Spv (A, IA). A continuous point of the valuation spectrum of a Huber ring lies in Spv (A, IA) for the extended ideal of definition of any pair of definition.

No finite-generation witness is asked of the caller: IA is finitely generated by TauCeti.Huber.PairOfDefinition.fg_extendedIdealOfDefinition, so the canonical one is supplied here.

source
theorem TauCeti.ValuationSpectrum.cont_subset_spvOfIdeal_extendedIdealOfDefinition {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) :
cont A ⊆ spvOfIdeal P.extendedIdealOfDefinition ⋯

Wedhorn Theorem 7.10, the inclusion Cont A ⊆ Spv (A, IA), as an inclusion of subsets.

source
theorem TauCeti.ValuationSpectrum.not_vle_one_of_isContinuous_of_mem_idealOfDefinition {A : Type u_1} [CommRing A] [TopologicalSpace A] (P : Huber.PairOfDefinition A) {v : ValuationSpectrum A} (hv : v.IsContinuous) {a : ↥P.ringOfDefinition} (ha : a ∈ P.idealOfDefinition) :
¬1 ≤ᵥ ↑a

A continuous point is sub-unit on the ideal of definition — the other conjunct of Wedhorn Theorem 7.10's inclusion ⊆, beside the membership mem_spvOfIdeal_extendedIdealOfDefinition_of_isContinuous above. An element of the ideal of definition is topologically nilpotent, and a continuous valuation takes a value < 1 at a topologically nilpotent element.

source
theorem TauCeti.ValuationSpectrum.isContinuous_of_mem_spvOfIdeal_of_forall_vlt_one {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) {v : ValuationSpectrum A} (hmem : v ∈ spvOfIdeal P.extendedIdealOfDefinition ⋯) (h1 : ∀ a ∈ P.idealOfDefinition, ↑a <ᵥ 1) :
v.IsContinuous

Wedhorn Theorem 7.10, the converse inclusion. A point of Spv (A, IA) that is sub-unit on the ideal of definition is continuous.

The sub-unit hypothesis quantifies over the ideal of definition I itself — through the subring inclusion — and not over the extension IA. The IA-form would be the stronger demand (the extension contains the image of I among much else), and it is not what Theorem 7.10's right-hand side supplies.

source
theorem TauCeti.ValuationSpectrum.cont_eq_spvOfIdeal_inter_setOfPred_forall_vlt_one {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) :
cont A = spvOfIdeal P.extendedIdealOfDefinition ⋯ ∩ {v : ValuationSpectrum A | ∀ a ∈ P.idealOfDefinition, ↑a <ᵥ 1}

Wedhorn Theorem 7.10. The continuous points of the valuation spectrum of a Huber ring are exactly the points of Spv (A, IA) that are sub-unit on the ideal of definition.

source
theorem TauCeti.ValuationSpectrum.isClosed_val_preimage_cont {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) :
IsClosed (Subtype.val ⁻¹' cont A)

Wedhorn Corollary 7.12. Cont A is a closed subset of Spv (A, IA): by Theorem 7.10 its trace on the subspace is the sub-unit locus of the ideal of definition, which is closed already in Spv A.