The adic spectrum of A⟨T/s⟩ is an open subspace of Spa (A, A⁺) #
For a rational subset R(T/s) of Spa (A, A⁺), the map j : Spa (A⟨T/s⟩, A_U⁺) → Spa (A, A⁺)
induced by the structure map A → A⟨T/s⟩ is an open embedding with range R(T/s). This is the
form of Wedhorn's Proposition 8.2 (2), first assertion, that the structure presheaves consume: the
presheaf of Spa (A, A⁺) restricted along j is a presheaf on Spa (A⟨T/s⟩, A_U⁺), whose value
at an open W is the value of the original presheaf at the image j(W).
The file records the calculus of images and preimages of opens along j — the pullback
locOpensComap is a left inverse of the image functor j'', and a right inverse of it on the
opens contained in R(T/s) — and that both carry rational opens to rational opens. Together with
exists_mem_spaRationalOpens_locOpensComap_eq this makes j'' a bijection from the rational opens
of Spa (A⟨T/s⟩, A_U⁺) onto the rational opens of Spa (A, A⁺) contained in R(T/s), which is
Proposition 8.2 (2), second assertion, for Opens.
Main definitions #
TauCeti.ValuationSpectrum.spaComapLocHom: the mapjas a morphism ofTopCat.
Main results #
TauCeti.ValuationSpectrum.isOpenEmbedding_spaComapLoc,TauCeti.ValuationSpectrum.isOpenEmbedding_spaComapLocHom:jis an open embedding.TauCeti.ValuationSpectrum.range_spaComapLoc: the range ofjisR(T/s).TauCeti.ValuationSpectrum.locOpensComap_spaComapLoc_functor_obj,TauCeti.ValuationSpectrum.spaComapLoc_functor_obj_locOpensComap:j⁻¹(j(W)) = W, andj(j⁻¹(V)) = VforV ⊆ R(T/s).TauCeti.ValuationSpectrum.spaComapLoc_functor_obj_mono,TauCeti.ValuationSpectrum.spaComapLoc_functor_obj_le_spaBasicOpen: the image alongjis monotone and lies inR(T/s).TauCeti.ValuationSpectrum.spaComapLoc_functor_obj_mem_spaRationalOpens,TauCeti.ValuationSpectrum.locOpensComap_mem_spaRationalOpens: images and preimages of rational opens alongjare rational opens.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 8.2 (2).
Spa (A⟨T/s⟩, A_U⁺) → Spa (A, A⁺) is an open embedding #
The range of j : Spa (A⟨T/s⟩, A_U⁺) → Spa (A, A⁺) is R(T/s), as a subset of
Spa (A, A⁺). The containment ⊆ is range_spaComapLoc_subset; equality is the surjectivity of
spaCompletedLocalizationHomeomorph onto the rational subset.
j : Spa (A⟨T/s⟩, A_U⁺) → Spa (A, A⁺) is an open embedding. It is the homeomorphism
spaCompletedLocalizationHomeomorph onto R(T/s) followed by the inclusion of that open
subset.
The map j : Spa (A⟨T/s⟩, A_U⁺) → Spa (A, A⁺) as a morphism of TopCat, the form in
which a presheafed space is restricted along it.
Equations
- TauCeti.ValuationSpectrum.spaComapLocHom P Aplus T s S hden = TopCat.ofHom { toFun := TauCeti.ValuationSpectrum.spaComapLoc P Aplus T s S hden, continuous_toFun := ⋯ }
Instances For
The morphism spaComapLocHom is the function spaComapLoc.
j : Spa (A⟨T/s⟩, A_U⁺) → Spa (A, A⁺) is an open embedding, for the morphism of
TopCat.
Images and preimages of opens along j #
The pullback of an open along j is the preimage of its underlying set.
Pulling back the image of an open along j gives the open back: j⁻¹(j(W)) = W, since
j is injective.
The image of the pullback of an open contained in R(T/s) is the open itself:
j(j⁻¹(V)) = V for V ⊆ R(T/s), since R(T/s) is the range of j.
The image along j preserves containment of opens. This is CategoryTheory.Functor.monotone
for the image functor of j, in the form the restriction maps between presentation limits
take as their argument.
The image along j of every open of Spa (A⟨T/s⟩, A_U⁺) lies in R(T/s).
Rational opens correspond #
The image along j of a rational open is a rational open, when T spans an open ideal.
This is the injectivity half of Wedhorn's Proposition 8.2 (2), second assertion, for Opens:
combined with exists_mem_spaRationalOpens_locOpensComap_eq, the pullback along j and the image
along j are inverse bijections between the rational opens of Spa (A, A⁺) contained in
R(T/s) and the rational opens of Spa (A⟨T/s⟩, A_U⁺).
The pullback along j of a rational open is a rational open. This is
spaComapLoc_preimage_mem_spaRationalFamily for Opens.