Rational subsets under a localization homeomorphism

Let S be a localization of A at a submonoid M. Every finite family of elements of S has a common denominator in M. Multiplying all the numerators and the denominator of a rational subset by that common denominator does not change the subset, because the multiplier is a unit. Thus every rational subset of Spa(S, S⁺) is cut out by elements coming from A.

This is the algebraic denominator-clearing part of Wedhorn Proposition 8.2(2), that a rational subset of a rational subset is rational in the original adic spectrum. Combined with the homeomorphism

Spa(A(T/s), A(T/s)⁺) ≃ R(T/s),

it says that any rational subset on the left is the inverse image of a basic rational locus in Spa(A, A⁺). Over Huber rings that locus is moreover presented admissibly: the cleared numerator family may be padded with a finite subset of A spanning an open ideal without changing its preimage in Spa(S, S⁺), so the presentation in A is one of a rational subset — that is, a member of the rational family spaRationalFamily. To obtain Proposition 8.2(2) in full, one must still pass from A(T/s) to the completed localization A⟨T/s⟩.

Main results

• TauCeti.ValuationSpectrum.exists_map_span_eq_and_comap_preimage_basicOpenFinset_eq: a rational open over a localization is the pullback of one presented by elements of the source ring, whose numerator ideal extends to the ideal generated by the original numerators and denominator.
• TauCeti.ValuationSpectrum.exists_mem_spaRationalFamily_spaComap_preimage_eq_of_isLocalization: every member of the rational family of Spa(S, S⁺) is the preimage under spaComap of a member of the rational family of Spa(A, A⁺).
• TauCeti.ValuationSpectrum.exists_mem_spaRationalFamily_spaLocalizationHomeomorph_preimage_eq: the same statement through the localization homeomorphism.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Proposition 8.2(2).
• For simultaneous denominator clearing in a localization, see Mathlib's IsLocalization.commonDenomOfFinset, IsLocalization.finsetIntegerMultiple, and IsLocalization.finsetIntegerMultiple_image.

theorem TauCeti.ValuationSpectrum.exists_map_span_eq_and_comap_preimage_basicOpenFinset_eq {A : Type u_1} {S : Type u_2} [CommRing A] [CommRing S] [Algebra A S] (M : Submonoid A) [IsLocalization M S] (U : Finset S) (q : S) : ∃ (V : Finset A) (r : A), Ideal.map (algebraMap A S) (Ideal.span ↑V) = Ideal.span (insert q ↑U) ∧ comap (algebraMap A S) ⁻¹' basicOpenFinset V r = basicOpenFinset U q

Clear denominators in a rational open of a localization. If S is a localization of A at a submonoid M, then every rational open Spv(S)(U/q) is the pullback of one presented by a finite family in A, and that family generates in S the ideal generated by U together with q.

No topological admissibility is asserted for the numerator family in A, and none is available here: padding a numerator family to span an open ideal fixes the locus only inside the adic spectrum, whereas this one lives in the whole valuation spectrum. It is the ideal identity that carries admissibility over to the cleared presentation, in TauCeti.ValuationSpectrum.exists_mem_spaRationalFamily_spaComap_preimage_eq_of_isLocalization.

theorem TauCeti.ValuationSpectrum.exists_mem_spaRationalFamily_spaComap_preimage_eq_of_isLocalization {A : Type u_1} {S : Type u_2} [CommRing A] [CommRing S] [Algebra A S] [TopologicalSpace A] [IsTopologicalRing A] [Huber.IsHuberRing A] [TopologicalSpace S] [IsTopologicalRing S] [Huber.IsHuberRing S] (M : Submonoid A) [IsLocalization M S] (Aplus : Subring A) (Bplus : Subring S) (hcont : Continuous ⇑(algebraMap A S)) (hplus : ∀ a ∈ Aplus, (algebraMap A S) a ∈ Bplus) {U : Set ↑(spa Bplus)} (hU : U ∈ spaRationalFamily Bplus) : ∃ W ∈ spaRationalFamily Aplus, spaComap (algebraMap A S) hcont Aplus Bplus hplus ⁻¹' W = U

Clear denominators in a rational subset of a localization. If S is a localization of A at a submonoid M, both Huber rings, then every member of the rational family of Spa(S, S⁺) is the preimage under spaComap (algebraMap A S) of a member of the rational family of Spa(A, A⁺); that is, R(T/s) = R(V/r) pulled back, with V · A open.

Denominator clearing produces a presentation in A of the underlying rational open, but says nothing about its numerator ideal. Openness is recovered afterwards: the numerators are padded by a finite subset of A spanning an open ideal. This can shrink the locus in Spa(A, A⁺), but does not change its preimage in Spa(S, S⁺).

theorem TauCeti.ValuationSpectrum.exists_mem_spaRationalFamily_spaLocalizationHomeomorph_preimage_eq {A : Type u_1} {S : Type u_2} [CommRing A] [CommRing S] [Algebra A S] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hP : P.ringOfDefinition ≤ Aplus) (T : Finset A) (s : A) [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (U : Set ↑(spa (integralClosure (↥(Algebra.adjoin (↥Aplus) (Set.range fun (t : ↥T) => Localization.divBy (↑t) s))) S).toSubring)) : U ∈ spaRationalFamily (integralClosure (↥(Algebra.adjoin (↥Aplus) (Set.range fun (t : ↥T) => Localization.divBy (↑t) s))) S).toSubring → ∃ W ∈ spaRationalFamily Aplus, ⇑(spaLocalizationHomeomorph P Aplus hP T s S hden) ⁻¹' Subtype.val ⁻¹' W = U

Rational subsets through the topological-localization homeomorphism. Every member of the rational family of Spa(A(T/s), A(T/s)⁺) is the inverse image, under the canonical homeomorphism with R(T/s), of the trace on R(T/s) of a member of the rational family of Spa(A, A⁺).

This is the denominator-clearing part of Wedhorn Proposition 8.2(2).