Standard rational families that cover the adic spectrum

Wedhorn, Adic Spaces (arXiv:1910.05934v1), Corollary 7.53.

For a finite subset T of a complete Hausdorff Huber pair (A, A⁺), the standard rational family (R(T/t))_{t ∈ T} is a covering of Spa (A, A⁺) exactly when T generates the unit ideal:

Ideal.span T = ⊤  ↔  Spa (A, A⁺) = ⋃ t ∈ T, R(T/t).

The → direction holds over an arbitrary commutative ring and is TauCeti.ValuationSpectrum.spa_eq_biUnion_rationalSubset_of_span_eq_top. The ← direction is the one that needs the pair: a point of the cover is nonzero on some t ∈ T, so no point of the spectrum kills all of T, and the support criterion TauCeti.ValuationSpectrum.span_eq_top_iff_forall_mem_spa_exists_notMem_supp turns that into the spanning statement. Completeness enters only through that criterion.

Main results

• TauCeti.ValuationSpectrum.span_eq_top_of_spa_eq_biUnion_rationalSubset : the ← direction.
• TauCeti.ValuationSpectrum.span_eq_top_iff_spa_eq_biUnion_rationalSubset : Wedhorn Corollary 7.53, the two directions together.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Corollary 7.53.

Provenance

Developed here; nothing is ported.

theorem TauCeti.ValuationSpectrum.span_eq_top_of_spa_eq_biUnion_rationalSubset {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 : Finset A} (hcov : spa Aplus = ⋃ t ∈ T, rationalSubset Aplus T t) : Ideal.span ↑T = ⊤

The converse half of Wedhorn Corollary 7.53. If the standard rational family (R(T/t))_{t ∈ T} covers Spa (A, A⁺) for a complete Hausdorff Huber pair, then T generates the unit ideal.

theorem TauCeti.ValuationSpectrum.span_eq_top_iff_spa_eq_biUnion_rationalSubset {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 : Finset A} : Ideal.span ↑T = ⊤ ↔ spa Aplus = ⋃ t ∈ T, rationalSubset Aplus T t

Wedhorn Corollary 7.53. A finite set T in a complete Hausdorff Huber pair generates the unit ideal exactly when the standard family (R(T/t))_{t ∈ T} covers Spa (A, A⁺).