Standard rational refinements of covers of the adic spectrum

Wedhorn, Adic Spaces (arXiv:1910.05934v1), Lemma 7.54, which is Huber's Lemma 2.6.

A finite set S generating the unit ideal gives the standard rational cover (R(S/f))_{f ∈ S} of Spa (A, A⁺) (Corollary 7.53). Lemma 7.54 says that an open cover of the adic spectrum has a standard rational refinement: some S generating the unit ideal with every R(S/f) inside a member of the cover.

Huber's proof multiplies presentations together. Let rational subsets R(Tᵢ/sᵢ) cover Spa (A, A⁺); since Spa (A, A⁺) is quasi-compact, finitely many of them suffice. Let S consist of the products ∏ᵢ tᵢ with tᵢ ∈ Tᵢ ∪ {sᵢ} for every i and tₖ = sₖ for at least one k. For such a product, R(S/∏ᵢ tᵢ) ⊆ R(Tₖ/sₖ). A point v of the left-hand side lies in some R(Tₗ/sₗ), so putting sₗ in the l-th slot does not lower the value of the product at v. Once sₗ is in the l-th slot, the k-th slot may hold any t ∈ Tₖ, and comparing with ∏ᵢ tᵢ bounds v(t) by v(sₖ). No point kills all of S, so S generates the unit ideal by Corollary 7.53.

That last step uses, at each point, an element of every Tᵢ that the point does not kill, which is automatic when every Tᵢ generates the unit ideal. In a Tate ring every open ideal is the unit ideal, so every rational subset has such a presentation.

Main results

• TauCeti.ValuationSpectrum.exists_span_eq_top_forall_rationalSubset_subset : a cover of Spa (A, A⁺) by rational subsets R(Tᵢ/sᵢ), each Tᵢ generating the unit ideal, has a standard rational refinement.
• TauCeti.ValuationSpectrum.exists_span_eq_top_forall_rationalSubset_subset_of_isTateRing : Wedhorn Lemma 7.54 over a complete Hausdorff Tate ring, for an arbitrary open cover.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Corollary 7.53 and Lemma 7.54.
• R. Huber, A generalization of formal schemes and rigid analytic varieties, Math. Z. 217 (1994), Lemma 2.6.
• AINTLIB, branch dev/adic-spaces, at commit 37bbdaeb9, projects/AdicSpaces/Adic spaces/WedhornCechAcyclicity.lean, section "Lemma 7.54".

Provenance

AINTLIB (github.com/CBirkbeck/AINTLIB @ 37bbdaeb9, Apache-2.0) carries out Huber's construction as distinguishedProducts, over a list of presentations each containing 1 among its numerators, and proves the refinement through the identity R(P/∏ᵢ tᵢ) = ⋂ᵢ R(Tᵢ/tᵢ) for the set P of all products. Here the presentations form an arbitrary family, cut down to a finite one by quasi-compactness, each numerator set is only assumed to generate the unit ideal, and the containment is proved directly by the two slot replacements described above; no AINTLIB code is copied.

theorem TauCeti.ValuationSpectrum.exists_span_eq_top_forall_rationalSubset_subset {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) {ι : Type u_2} {T : ι → Finset A} {s : ι → A} (hT : ∀ (i : ι), Ideal.span ↑(T i) = ⊤) (hcov : spa Aplus ⊆ ⋃ (i : ι), rationalSubset Aplus (T i) (s i)) : ∃ (S : Finset A), Ideal.span ↑S = ⊤ ∧ ∀ f ∈ S, ∃ (i : ι), rationalSubset Aplus S f ⊆ rationalSubset Aplus (T i) (s i)

A standard rational refinement of a rational cover. This is Wedhorn Lemma 7.54 (Huber Lemma 2.6) for a cover of Spa (A, A⁺) by rational subsets R(Tᵢ/sᵢ) whose numerator sets Tᵢ generate the unit ideal: some finite S generating the unit ideal has every R(S/f), f ∈ S, inside one of the R(Tᵢ/sᵢ). The cover may be infinite, since Spa (A, A⁺) is quasi-compact. The R(S/f) cover Spa (A, A⁺) by spa_eq_biUnion_rationalSubset_of_span_eq_top, so they form a standard rational cover refining the given one.

Wedhorn's rational subsets only ask the numerator ideals Tᵢ · A to be open, which is weaker. Over a Tate ring an open ideal is the unit ideal, and exists_span_eq_top_forall_rationalSubset_subset_of_isTateRing uses this to refine an arbitrary open cover of spa Aplus when A is a complete Hausdorff Tate ring.

theorem TauCeti.ValuationSpectrum.exists_span_eq_top_forall_rationalSubset_subset_of_isTateRing {A : Type u_1} [CommRing A] [UniformSpace A] [T2Space A] [CompleteSpace A] [IsTopologicalRing A] [IsUniformAddGroup A] [Huber.IsTateRing A] (Aplus : Subring A) (hplus : Huber.IsRingOfIntegralElements Aplus) {ι : Type u_2} (V : ι → Set ↑(spa Aplus)) (hV : ∀ (i : ι), IsOpen (V i)) (hcov : ⋃ (i : ι), V i = Set.univ) : ∃ (S : Finset A), Ideal.span ↑S = ⊤ ∧ ∀ f ∈ S, ∃ (i : ι), Subtype.val ⁻¹' rationalSubset Aplus S f ⊆ V i

Wedhorn Lemma 7.54 over a complete Hausdorff Tate ring: every open cover of Spa (A, A⁺) has a standard rational refinement, a finite S generating the unit ideal with every R(S/f), f ∈ S, inside a member of the cover. The R(S/f) cover Spa (A, A⁺) by spa_eq_biUnion_rationalSubset_of_span_eq_top. Over any complete Hausdorff Huber ring, exists_span_eq_top_forall_rationalSubset_subset gives such a refinement of a cover by rational subsets whose numerator sets generate the unit ideal.