Proper ideals of a complete Huber pair are contained in supports

Over a complete Hausdorff Huber pair (A, A⁺) every proper ideal J of A is contained in the support of some point of Spa (A, A⁺):

J ≠ ⊤  ↔  ∃ v ∈ Spa (A, A⁺), J ⊆ supp v.

This is Wedhorn's Proposition 7.51 in the form his §8 uses; for a maximal ideal the containment is an equality. Its standard consequence proved here is the unit criterion of Proposition 7.52(2). Corollary 7.53, which characterizes when a finite set's standard rational family covers the spectrum, is read off from it in TauCeti/AlgebraicGeometry/AdicSpace/Spa/RationalSubset/Cover.lean.

Comparison with the open-prime approach

TauCeti.ValuationSpectrum.exists_mem_spa_supp_eq produces a point with prescribed support from an open prime ideal, using the trivial valuation there, and the derived isUnit_of_forall_not_vle_zero and span_eq_top_of_forall_mem_spa_exists_not_vle_zero inherit an openness hypothesis on the maximal ideals of A. That hypothesis is unsatisfiable over a nonzero Tate ring, where an ideal is open exactly when it is ⊤ (TauCeti.Huber.IsTateRing.isOpen_iff_eq_top), so those statements are vacuous on the affinoid rings Wedhorn's §8 is about. The quotient-spectrum approach instead uses the following facts:

• the quotient Huber pair (A/J, (A/J)⁺) is again a Huber pair (TauCeti.Huber.Pair.quotient), and its spectrum is empty exactly when 1 lies in the closure of zero (TauCeti.ValuationSpectrum.spa_eq_empty_iff_one_mem_closure_zero, Wedhorn Proposition 7.49(1));
• completeness keeps a proper ideal from being dense, upstairs and downstairs alike (TauCeti.Huber.one_notMem_closure_zero_quotient_of_ne_top), because the unit group of a complete Huber ring is open;
• a point of the quotient spectrum is a point of Spa (A, A⁺) whose support contains J, which is the range computation TauCeti.ValuationSpectrum.range_spaComap_quotientMk.

Completeness replaces openness of the maximal ideals, and is exactly the hypothesis Wedhorn carries.

Main results

• TauCeti.ValuationSpectrum.exists_mem_spa_le_supp_of_ne_top : Wedhorn Proposition 7.51 — a proper ideal of a complete Hausdorff Huber pair is contained in the support of a point, with TauCeti.ValuationSpectrum.ne_top_iff_exists_mem_spa_le_supp the resulting criterion.
• TauCeti.ValuationSpectrum.exists_mem_spa_supp_eq_of_isMaximal : a maximal ideal is the support of a point.
• TauCeti.ValuationSpectrum.span_eq_top_iff_forall_mem_spa_exists_notMem_supp : a set generates the unit ideal exactly when no point of the spectrum kills all of it.
• TauCeti.ValuationSpectrum.isUnit_iff_forall_mem_spa_notMem_supp : Wedhorn Proposition 7.52(2), as a criterion.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Propositions 7.49, 7.51 and 7.52.

Provenance

Developed here. AINTLIB reaches Propositions 7.51 and 7.52(2) through an open maximal ideal, which is the route TauCeti/AlgebraicGeometry/AdicSpace/Spa/Points.lean carries over; the argument below shares nothing with it beyond the statements.

theorem TauCeti.ValuationSpectrum.exists_mem_spa_le_supp_of_ne_top {A : Type u_1} [CommRing A] [UniformSpace A] [T2Space A] [CompleteSpace A] [IsTopologicalRing A] [IsUniformAddGroup A] [Huber.IsHuberRing A] (Aplus : Subring A) (hplus : Huber.IsRingOfIntegralElements Aplus) {J : Ideal A} (hJ : J ≠ ⊤) : ∃ v ∈ spa Aplus, J ≤ v.supp

Wedhorn Proposition 7.51. Every proper ideal of a complete Hausdorff Huber pair is contained in the support of a point of Spa (A, A⁺). Wedhorn states the maximal-ideal case, where the containment is an equality.

theorem TauCeti.ValuationSpectrum.ne_top_iff_exists_mem_spa_le_supp {A : Type u_1} [CommRing A] [UniformSpace A] [T2Space A] [CompleteSpace A] [IsTopologicalRing A] [IsUniformAddGroup A] [Huber.IsHuberRing A] (Aplus : Subring A) (hplus : Huber.IsRingOfIntegralElements Aplus) (J : Ideal A) : J ≠ ⊤ ↔ ∃ v ∈ spa Aplus, J ≤ v.supp

A proper ideal of a complete Hausdorff Huber pair is exactly one contained in the support of some point of Spa (A, A⁺).

theorem TauCeti.ValuationSpectrum.exists_mem_spa_supp_eq_of_isMaximal {A : Type u_1} [CommRing A] [UniformSpace A] [T2Space A] [CompleteSpace A] [IsTopologicalRing A] [IsUniformAddGroup A] [Huber.IsHuberRing A] (Aplus : Subring A) (hplus : Huber.IsRingOfIntegralElements Aplus) (𝔪 : Ideal A) [𝔪.IsMaximal] : ∃ v ∈ spa Aplus, v.supp = 𝔪

Wedhorn Proposition 7.51, for a maximal ideal. A maximal ideal of a complete Hausdorff Huber pair is the support of a point of Spa (A, A⁺).

theorem TauCeti.ValuationSpectrum.span_eq_top_iff_forall_mem_spa_exists_notMem_supp {A : Type u_1} [CommRing A] [UniformSpace A] [T2Space A] [CompleteSpace A] [IsTopologicalRing A] [IsUniformAddGroup A] [Huber.IsHuberRing A] (Aplus : Subring A) (hplus : Huber.IsRingOfIntegralElements Aplus) {T : Set A} : Ideal.span T = ⊤ ↔ ∀ v ∈ spa Aplus, ∃ t ∈ T, t ∉ v.supp

A subset of a complete Hausdorff Huber pair generates the unit ideal exactly when no point of Spa (A, A⁺) kills all of it.

theorem TauCeti.ValuationSpectrum.isUnit_iff_forall_mem_spa_notMem_supp {A : Type u_1} [CommRing A] [UniformSpace A] [T2Space A] [CompleteSpace A] [IsTopologicalRing A] [IsUniformAddGroup A] [Huber.IsHuberRing A] (Aplus : Subring A) (hplus : Huber.IsRingOfIntegralElements Aplus) (f : A) : IsUnit f ↔ ∀ v ∈ spa Aplus, f ∉ v.supp

Wedhorn Proposition 7.52(2). An element of a complete Hausdorff Huber pair is a unit exactly when no point of Spa (A, A⁺) vanishes on it.