The integral sections of the presentation-limit pre-adic space #
For a Huber pair (A, A⁺), the integral sections 𝒪_X⁺(V) of the pre-adic space
presentationLimitPreAdicSpace on X = Spa(A, A⁺), defined through its stalk valuations, are the
plus subrings presentationLimitPlusSubring of the presentation-limit presheaf. On a rational open
R(T/s) these are the plus ring A_U⁺ of the coordinate ring A⟨T/s⟩ (Wedhorn,
Proposition 8.16).
Main results #
TauCeti.ValuationSpectrum.presentationLimitPreAdicSpace_plusSubring: onSpa(A, A⁺)the integral sections arepresentationLimitPlusSubring.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), §8.1 and Proposition 8.16.
theorem
TauCeti.ValuationSpectrum.presentationLimitPreAdicSpace_plusSubring
{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)
(V : TopologicalSpace.Opens ↑(spa Aplus))
:
(presentationLimitPreAdicSpace P Aplus hAplus hP).plusSubring V = presentationLimitPlusSubring hAplus hP V
The integral sections of Spa(A, A⁺) are the plus subrings presentationLimitPlusSubring
of the presentation-limit presheaf. On a rational open R(T/s) these are the plus ring A_U⁺ of
A⟨T/s⟩, by map_completedPlusSubring_eq_presentationLimitPlusSubring.