Rational subsets are open affinoid subspaces

Let X = Spa(A, A⁺) be the presentation-limit pre-adic space of A with a plus ring A⁺ of power-bounded elements containing the ring of definition, let U = R(T/s) be a rational subset with T spanning an open ideal, and let j : Spa(A⟨T/s⟩, A_U⁺) → X be the open embedding induced by the structure map A → A⟨T/s⟩. This file proves that the restriction of X along j is isomorphic in 𝒱^pre to the pre-adic space Spa(A⟨T/s⟩, A_U⁺), Wedhorn's Remark 8.8. The underlying isomorphism of presheafed spaces is Wedhorn's Remark 8.4, presentationLimitPresheafLocIso; what is added here is the compatibility of the stalk valuations, which makes it an isomorphism of pre-adic spaces.

Consequently every rational open of X is an open affinoid subspace, and when A is a Huber ring the open affinoid subspaces of X form a basis of its topology. That is the basis hypothesis of TauCeti.PreAdicSpace.isSheafy_of_isAdapted_of_isSheaf_affinoidOpens, under which the sheaf condition can be checked on open affinoid subspaces. Since the whole space is rational and the structure presheaf is adapted to the rational opens, hence to the larger family of open affinoid subspaces, X is a pre-adic space in Wedhorn's sense.

The stalk valuations

The valuation on the stalk at a point is determined by its pullbacks along the germ maps of the rational neighbourhoods of the point (eq_presentationLimitStalkValuation). For a rational neighbourhood R(p') of y in Spa(A⟨T/s⟩, A_U⁺), present j(R(p')) by p. The germ maps of R(p') at y and of R(p) at j(y) correspond under the ring isomorphism A⟨p⟩ ≅ A⟨T/s⟩⟨p'⟩ of Remark 8.4, and that isomorphism matches the points of the two coordinate rings determined by j(y) and by y (comap_presentationLimitLocIso_rationalLocalizationPoint).

Main definitions

• TauCeti.ValuationSpectrum.presentationLimitPreAdicSpaceLocIso: the isomorphism in 𝒱^pre between the restriction of Spa(A, A⁺) along j and Spa(A⟨T/s⟩, A_U⁺).

Main results

• TauCeti.ValuationSpectrum.isAffinoid_restrict_spaComapLocHom: the restriction of Spa(A, A⁺) along j is an affinoid pre-adic space.
• TauCeti.ValuationSpectrum.spaBasicOpen_mem_affinoidOpens, TauCeti.ValuationSpectrum.spaRationalOpens_subset_affinoidOpens: rational subsets are open affinoid subspaces.
• TauCeti.ValuationSpectrum.isBasis_affinoidOpens_presentationLimitPreAdicSpace: the open affinoid subspaces form a basis of the topology.
• TauCeti.ValuationSpectrum.isPreAdic_presentationLimitPreAdicSpace, TauCeti.PreAdicSpace.isPreAdic_of_isAffinoid: Spa(A, A⁺), and hence every affinoid pre-adic space, is a pre-adic space, Wedhorn's Remark and Definition 8.10.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Remarks 8.4 and 8.8 and Remark and Definition 8.10.

noncomputable def TauCeti.ValuationSpectrum.presentationLimitPreAdicSpaceLocIso {A : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (T : Finset A) (s : A) (S : Type u) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (hP : P.ringOfDefinition ≤ Aplus) (hT : IsOpen ↑(Ideal.span ↑T)) : (presentationLimitPreAdicSpace P Aplus hAplus hP).restrict ⋯ ≅ presentationLimitPreAdicSpace (P.completionLocalization T s S hden) (P.completedPlusSubring Aplus T s S hden) ⋯ ⋯

Wedhorn's Remark 8.8 for the presentation-limit pre-adic spaces. Let U = R(T/s) be a rational subset of X = Spa(A, A⁺), where T spans an open ideal, A⁺ consists of power-bounded elements and contains the ring of definition, and let j : Spa(A⟨T/s⟩, A_U⁺) → X be the open embedding induced by the structure map. The restriction of the pre-adic space X along j is isomorphic in 𝒱^pre to the pre-adic space Spa(A⟨T/s⟩, A_U⁺): the isomorphism is the identity on points, it is presentationLimitPresheafLocIso on sections (presentationLimitPreAdicSpaceLocIso_hom_toHom), and it matches the stalk valuations.

Equations

• TauCeti.ValuationSpectrum.presentationLimitPreAdicSpaceLocIso P Aplus T s S hden hAplus hP hT = CategoryTheory.asIso (TauCeti.ValuationSpectrum.restrictLocHom✝ P Aplus T s S hden hAplus hP hT)

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitPreAdicSpaceLocIso_hom_base {A : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (T : Finset A) (s : A) (S : Type u) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (hP : P.ringOfDefinition ≤ Aplus) (hT : IsOpen ↑(Ideal.span ↑T)) : (presentationLimitPreAdicSpaceLocIso P Aplus T s S hden hAplus hP hT).hom.base = CategoryTheory.CategoryStruct.id ↑((presentationLimitPreAdicSpace P Aplus hAplus hP).restrict ⋯).toPresheafedSpace

On points, presentationLimitPreAdicSpaceLocIso is the identity.

theorem TauCeti.ValuationSpectrum.presentationLimitPreAdicSpaceLocIso_hom_toHom {A : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (T : Finset A) (s : A) (S : Type u) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (hP : P.ringOfDefinition ≤ Aplus) (hT : IsOpen ↑(Ideal.span ↑T)) : (presentationLimitPreAdicSpaceLocIso P Aplus T s S hden hAplus hP hT).hom.toHom = (AlgebraicGeometry.PresheafedSpace.isoOfComponents (CategoryTheory.Iso.refl ↑((presentationLimitPreAdicSpace P Aplus hAplus hP).restrict ⋯).toPresheafedSpace) (presentationLimitPresheafLocIso P Aplus T s S hden hAplus hP hT)).hom

The underlying isomorphism of presheafed spaces of presentationLimitPreAdicSpaceLocIso is the identity on points together with presentationLimitPresheafLocIso, Wedhorn's Remark 8.4 for the presentation-limit presheaves, on sections.

theorem TauCeti.ValuationSpectrum.isAffinoid_restrict_spaComapLocHom {A : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (T : Finset A) (s : A) (S : Type u) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (hP : P.ringOfDefinition ≤ Aplus) (hT : IsOpen ↑(Ideal.span ↑T)) : ((presentationLimitPreAdicSpace P Aplus hAplus hP).restrict ⋯).isAffinoid

The restriction of Spa(A, A⁺) along j : Spa(A⟨T/s⟩, A_U⁺) → Spa(A, A⁺) is an affinoid pre-adic space, isomorphic in 𝒱^pre to the pre-adic space of the Huber pair (A⟨T/s⟩, A_U⁺).

theorem TauCeti.ValuationSpectrum.spaBasicOpen_mem_affinoidOpens {A : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (hP : P.ringOfDefinition ≤ Aplus) {T : Finset A} {s : A} (hT : IsOpen ↑(Ideal.span ↑T)) : spaBasicOpen Aplus T s ∈ (presentationLimitPreAdicSpace P Aplus hAplus hP).affinoidOpens

Rational subsets are open affinoid subspaces. For T spanning an open ideal, the rational subset R(T/s) of the presentation-limit pre-adic space Spa(A, A⁺) is an open affinoid subspace: the restriction to it is isomorphic in 𝒱^pre to Spa(A⟨T/s⟩, A_U⁺).

theorem TauCeti.ValuationSpectrum.spaRationalOpens_subset_affinoidOpens {A : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (hP : P.ringOfDefinition ≤ Aplus) : spaRationalOpens Aplus ⊆ (presentationLimitPreAdicSpace P Aplus hAplus hP).affinoidOpens

Every rational open is an open affinoid subspace of the presentation-limit pre-adic space Spa(A, A⁺).

theorem TauCeti.ValuationSpectrum.isBasis_affinoidOpens_presentationLimitPreAdicSpace {A : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (hP : P.ringOfDefinition ≤ Aplus) [Huber.IsHuberRing A] : TopologicalSpace.Opens.IsBasis (presentationLimitPreAdicSpace P Aplus hAplus hP).affinoidOpens

The open affinoid subspaces of Spa(A, A⁺) form a basis of its topology, since the rational opens do. This is the basis hypothesis of TauCeti.PreAdicSpace.isSheafy_of_isAdapted_of_isSheaf_affinoidOpens.

theorem TauCeti.ValuationSpectrum.isPreAdic_presentationLimitPreAdicSpace {A : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (hP : P.ringOfDefinition ≤ Aplus) : (presentationLimitPreAdicSpace P Aplus hAplus hP).isPreAdic

Spa(A, A⁺) is a pre-adic space (Wedhorn, Remark and Definition 8.10): the presentation-limit pre-adic space of A with a plus ring A⁺ of power-bounded elements containing the ring of definition is locally affinoid, since the whole space is a rational open and so an open affinoid subspace, and its structure presheaf is adapted to the open affinoid subspaces, since it is adapted to the rational opens, which are among them.

theorem TauCeti.PreAdicSpace.isPreAdic_of_isAffinoid {X : PreAdicSpace} (hX : X.isAffinoid) : X.isPreAdic

Affinoid pre-adic spaces are pre-adic spaces (Wedhorn, Remark and Definition 8.10): an object of 𝒱^pre isomorphic to some Spa(A, A⁺) is locally affinoid with structure presheaf adapted to its open affinoid subspaces.