Rational subsets of the completed rational localization #
For a rational subset R(T/s) of Spa (A, A⁺), spaCompletedLocalizationHomeomorph identifies
Spa (A⟨T/s⟩, A_U⁺) with R(T/s). This file shows that the identification matches rational
subsets: pullback along the structure map ρ : A → A⟨T/s⟩ is a bijection between the rational
subsets of Spa (A, A⁺) contained in R(T/s) and the rational subsets of Spa (A⟨T/s⟩, A_U⁺).
That is the second assertion of Wedhorn, Adic Spaces, Proposition 8.2 (2); the first assertion
is the homeomorphism itself.
The argument factors the ring homomorphism rather than the homeomorphism. The structure map is
the composite A → Aₛ → A⟨T/s⟩ of the localization map with the completion map, so spaComapLoc
is the composite of the two corresponding spaComaps — this is
TauCeti.ValuationSpectrum.spaComapLoc_eq_comp in Spa/Localization/Basic.lean, and it is what
the two descent results below rewrite with. Each factor carries rational subsets in both
directions: the localization factor by clearing denominators, the completion factor because the
completion map has dense range. The structure map itself need not have dense range — A is in
general not dense in Aₛ — so the factorization is not a convenience but the route.
No completeness, Tate or Noetherian hypothesis is needed, and A⁺ is an arbitrary subring
subject only to the hypothesis A₀ ≤ A⁺ that the homeomorphism already carries.
Main definitions #
TauCeti.ValuationSpectrum.locOpensComap: the pullback of an open ofSpa (A, A⁺)alongspaComapLoc, as an open ofSpa (A⟨T/s⟩, A_U⁺).
Main results #
TauCeti.ValuationSpectrum.locOpensComap_spaBasicOpen: the pullback of the basic openR(T'/s')isR(ρ(T')/ρ(s')); the pullback ofR(T/s)itself is the whole spectrum (TauCeti.ValuationSpectrum.locOpensComap_spaBasicOpen_self), that is,R(ρ(T)/ρ(s))is all ofSpa (A⟨T/s⟩, A_U⁺)(TauCeti.ValuationSpectrum.spaBasicOpen_image_toCompletionLoc_eq_top).TauCeti.ValuationSpectrum.spaComapLoc_preimage_mem_spaRationalFamilyandTauCeti.ValuationSpectrum.exists_mem_spaRationalFamily_spaComapLoc_preimage_eq: the rational subsets ofSpa (A⟨T/s⟩, A_U⁺)are exactly the preimages underρof the rational subsets ofSpa (A, A⁺).TauCeti.ValuationSpectrum.spaCompletedLocalizationHomeomorph_preimage_mem_spaRationalFamily,exists_mem_spaRationalFamily_spaCompletedLocalizationHomeomorph_preimage_eqandTauCeti.ValuationSpectrum.spaCompletedLocalizationHomeomorph_image_mem_spaRationalFamily: the same two statements phrased through the homeomorphism, together with the image form.TauCeti.ValuationSpectrum.bijOn_preimage_spaCompletedLocalizationHomeomorph_spaRationalFamily: Wedhorn Proposition 8.2 (2), second assertion — the bijection between the rational subsets ofSpa (A, A⁺)contained inR(T/s)and the rational subsets ofSpa (A⟨T/s⟩, A_U⁺).TauCeti.ValuationSpectrum.exists_mem_spaRationalOpens_locOpensComap_eq: its surjectivity half forOpens, for every subringA⁺— each rational open ofSpa (A⟨T/s⟩, A_U⁺)islocOpensComapof a rational open ofSpa (A, A⁺)contained inR(T/s).
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 8.2 (2), second assertion.
Rational subsets pull back to rational subsets along the structure map. The preimage
under ρ : A → A⟨T/s⟩ of a member of the rational family of Spa (A, A⁺) is a member of the
rational family of Spa (A⟨T/s⟩, A_U⁺).
Every rational subset of Spa (A⟨T/s⟩, A_U⁺) is pulled back from one of Spa (A, A⁺).
This is the substantial direction of Wedhorn Proposition 8.2 (2).
The rational subset obtained downstairs need not be contained in R(T/s); only its trace on
R(T/s) is determined.
Rational subsets pull back to rational subsets through the homeomorphism. The preimage
under spaCompletedLocalizationHomeomorph of the trace on R(T/s) of a member of the rational
family of Spa (A, A⁺) is a member of the rational family of Spa (A⟨T/s⟩, A_U⁺).
Every rational subset of Spa (A⟨T/s⟩, A_U⁺) is pulled back through the homeomorphism.
The homeomorphism-phrased form of exists_mem_spaRationalFamily_spaComapLoc_preimage_eq.
Rational subsets push forward to rational subsets through the homeomorphism. The image in
Spa (A, A⁺) of a member of the rational family of Spa (A⟨T/s⟩, A_U⁺) is a member of the
rational family of Spa (A, A⁺).
The image is automatically contained in R(T/s), and it is the openness of the numerator ideal
of R(T/s) that keeps the intersection with R(T/s) inside the rational family.
Wedhorn, Adic Spaces, Proposition 8.2 (2), second assertion. Pullback along the
structure map ρ : A → A⟨T/s⟩ is a bijection between the rational subsets of Spa (A, A⁺)
contained in R(T/s) and the rational subsets of Spa (A⟨T/s⟩, A_U⁺).
The statement is a Set.BijOn rather than an Iff between memberships because the codomain of
the homeomorphism is the subtype ↥R(T/s): pullback is not injective on all subsets of
Spa (A, A⁺), since two rational subsets with the same trace on R(T/s) have the same preimage.
Restricting the domain to the rational subsets contained in R(T/s) is what makes it injective,
and every rational subset of Spa (A⟨T/s⟩, A_U⁺) is still hit, because a rational subset may be
intersected with R(T/s) without changing its preimage.
Pulling back opens along the structure map #
The pullback of an open along Spa of the structure map: for an open V of Spa (A, A⁺),
the open j⁻¹(V) of Spa (A⟨T/s⟩, A_U⁺), where j = spaComapLoc is induced by the structure map
A → A⟨T/s⟩. Membership is mem_locOpensComap.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A point of Spa (A⟨T/s⟩, A_U⁺) lies in locOpensComap … V exactly when its image under
spaComapLoc lies in V.
Pulling back along spaComapLoc preserves containment of opens.
The pullback of a basic open: pulling R(T'/s') back along spaComapLoc gives the basic
open R(ρ(T')/ρ(s')) of Spa (A⟨T/s⟩, A_U⁺), where ρ : A → A⟨T/s⟩ is the structure map.
Pulling back along spaComapLoc commutes with intersections of opens.
The pullback of R(T/s) is the whole spectrum. Every point of Spa (A⟨T/s⟩, A_U⁺) lies
over R(T/s) (spaComapLoc_mem_rationalSubset), so pulling R(T/s) back along spaComapLoc
gives all of Spa (A⟨T/s⟩, A_U⁺).
R(ρ(T)/ρ(s)) is all of Spa (A⟨T/s⟩, A_U⁺), where ρ : A → A⟨T/s⟩ is the structure
map. This is locOpensComap_spaBasicOpen_self with its left side in the form to which
locOpensComap_spaBasicOpen rewrites the pullback of R(T/s).
Every rational open of Spa (A⟨T/s⟩, A_U⁺) is the pullback of a rational open of
Spa (A, A⁺) contained in R(T/s), when T spans an open ideal. This is the surjectivity half
of Wedhorn's Proposition 8.2 (2)
(bijOn_preimage_spaCompletedLocalizationHomeomorph_spaRationalFamily), stated for Opens and
for the pullback locOpensComap along spaComapLoc; unlike that statement, it holds for every
subring A⁺, with no hypothesis P.ringOfDefinition ≤ A⁺. In contrast to the set-level
exists_mem_spaRationalFamily_spaComapLoc_preimage_eq, the rational open it provides in
Spa (A, A⁺) lies inside R(T/s).