Wedhorn's chain of rational subsets

Wedhorn, Adic Spaces (arXiv:1910.05934v1), Remark 7.55.

Wedhorn refines a rational subset U = R(T/s) into a descending chain of rational subsets

Spa (A, A⁺) ⊇ X₀ ⊇ X₁ ⊇ ⋯ ⊇ Xₙ = U

in which every step adjoins a single numerator: X₀ = R({u}/s) for an element u dominated by s throughout U, and Xᵢ adjoins the i-th element of T. The point of the chain is that each of its steps is an elementary one, so a statement about restriction maps between rational localisations that is stable under composition need only be proved for a single adjoined numerator; this is how Wedhorn's Proposition 8.30 reduces flatness to an elementary case.

The dominating element

Wedhorn obtains u from quasi-compactness of U via his Corollary 7.32, which produces a unit u ∈ Aˣ with |u(x)| < |s(x)| on U, and writes the first link as X₀ = {x ∈ Spa A; 1 ≤ x(s/u)}. That description presupposes u invertible, in order to form the fraction s/u. Here u : A is an arbitrary ring element and X₀ is the rational subset R({u}/s), which is the same set whenever u is a unit: R({u}/s) asks for v(u) ≤ v(s) together with v(s) ≠ 0, and for a unit the second condition follows from the first, since v(u) ≠ 0. Nothing in the chain needs invertibility, so it is not assumed; a caller holding Corollary 7.32's unit ϖ applies these results with u := (ϖ : A).

Strictness is likewise not needed. Wedhorn's u satisfies v(u) < v(s) on U, but the chain only ever consumes the non-strict v(u) ≤ v(s), so that is what the results below assume; a caller holding the strict form passes (hu v hv).vle.

Quasi-compactness of U is likewise not a hypothesis here. It is the input to Corollary 7.32, and enters only when a caller discharges the domination hypothesis by that route.

Main results

• TauCeti.ValuationSpectrum.exists_rationalSubset_chain : Remark 7.55 itself — the descending chain of rational subsets from R({u}/s) down to R(T/s), each step adjoining one element of T.

References

• Wedhorn, Adic Spaces, Remark 7.55.

theorem TauCeti.ValuationSpectrum.exists_rationalSubset_chain {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (T : Finset A) (s u : A) (hu : ∀ v ∈ rationalSubset Aplus T s, u ≤ᵥ s) : ∃ (N : ℕ → Finset A), N 0 = {u} ∧ (∀ (i : ℕ), rationalSubset Aplus (N i) s ⊆ spa Aplus) ∧ (Antitone fun (i : ℕ) => rationalSubset Aplus (N i) s) ∧ (∀ i < T.card, ∃ t ∈ T, N (i + 1) = insert t (N i)) ∧ rationalSubset Aplus (N T.card) s = rationalSubset Aplus T s

Wedhorn Remark 7.55: the chain of rational subsets. Let u be dominated by s throughout U = R(T/s). Then there is a descending chain of rational subsets

Spa (A, A⁺) ⊇ R({u}/s) = X₀ ⊇ X₁ ⊇ ⋯ ⊇ X_{#T} = U

whose every step adjoins a single element of T to the numerators.

The chain is exhibited by its numerator sets N i, each Xᵢ being R(N i / s), so that every member is a rational subset by construction rather than by a separate argument. The enumeration of T is Finset.toList; any enumeration would do, and the statement fixes one only so that the i-th step has a name.