Units of a rational coordinate ring near a point

Let U = R(T/s) be a rational subset of Spa (A, A⁺) with coordinate ring A⟨T/s⟩. For a point x ∈ U, write x_U for the point of Spa (A⟨T/s⟩, A_U⁺) lying over x under the homeomorphism spaCompletedLocalizationHomeomorph of Wedhorn's Proposition 8.2 (2). This file proves that f ∈ A⟨T/s⟩ does not vanish at x_U, that is f ∉ supp x_U, exactly when f becomes a unit in the coordinate ring of some rational neighbourhood R(T'/s') ⊆ R(T/s) of x.

This criterion supplies the local unit calculation for proving that the stalk of the structure presheaf at x is a local ring whose maximal ideal is the support of the point valuation.

Main results

• ringHomOfRationalSubsetSubset_mem_supp_iff: vanishing at x is compatible with restriction — for R(T'/s') ⊆ R(T/s), f vanishes at x_U exactly when its image in A⟨T'/s'⟩ vanishes at x_U'.
• notMem_supp_of_isUnit_ringHomOfRationalSubsetSubset: an element that becomes a unit on a rational neighbourhood of x does not vanish at x.
• notMem_supp_iff_exists_isUnit_ringHomOfRationalSubsetSubset: the criterion — f does not vanish at x exactly when it becomes a unit on a rational neighbourhood of x, which may be taken with an admissible presentation.
• isUnit_toCompletionLoc_iff_forall_notMem_supp: an element of A becomes a unit in A⟨T/s⟩ exactly when it vanishes at no point of R(T/s).

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Propositions 7.52 and 8.2, and §8.1.

@[simp]

theorem TauCeti.ValuationSpectrum.ringHomOfRationalSubsetSubset_mem_supp_iff {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hP : P.ringOfDefinition ≤ Aplus) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s' S'] (hden' : P.HasDenominatorPower T' s' S') (hsub : rationalSubset Aplus T' s' ⊆ rationalSubset Aplus T s) (x : ↑(Subtype.val ⁻¹' rationalSubset Aplus T' s')) (f : UniformSpace.Completion S) : (ringHomOfRationalSubsetSubset P Aplus hAplus T s S hden T' s' S' hden' hsub) f ≤ᵥ 0 ↔ f ≤ᵥ 0

Vanishing at x is compatible with restriction. For a containment R(T'/s') ⊆ R(T/s) and a point x ∈ R(T'/s'), the image of f ∈ A⟨T/s⟩ in A⟨T'/s'⟩ lies in the support of the point over x exactly when f does.

theorem TauCeti.ValuationSpectrum.notMem_supp_of_isUnit_ringHomOfRationalSubsetSubset {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hP : P.ringOfDefinition ≤ Aplus) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s' S'] (hden' : P.HasDenominatorPower T' s' S') (hsub : rationalSubset Aplus T' s' ⊆ rationalSubset Aplus T s) (x : ↑(Subtype.val ⁻¹' rationalSubset Aplus T' s')) (f : UniformSpace.Completion S) : IsUnit ((ringHomOfRationalSubsetSubset P Aplus hAplus T s S hden T' s' S' hden' hsub) f) → f ∉ (↑((spaCompletedLocalizationHomeomorph P Aplus hP T s S hden).symm (Set.inclusion ⋯ x))).supp

If f ∈ A⟨T/s⟩ becomes a unit in the coordinate ring of a rational subset R(T'/s') ⊆ R(T/s), then f vanishes at no point of R(T'/s').

theorem TauCeti.ValuationSpectrum.notMem_supp_iff_exists_isUnit_ringHomOfRationalSubsetSubset {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hP : P.ringOfDefinition ≤ Aplus) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (T : Finset A) (s : A) (hT : IsOpen ↑(Ideal.span ↑T)) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (x : ↑(Subtype.val ⁻¹' rationalSubset Aplus T s)) (f : UniformSpace.Completion S) : f ∉ (↑((spaCompletedLocalizationHomeomorph P Aplus hP T s S hden).symm x)).supp ↔ ∃ (q : P.Presentation), IsOpen ↑(Ideal.span ↑q.num) ∧ ↑↑x ∈ rationalSubset Aplus q.num q.den ∧ ∃ (hsub : rationalSubset Aplus q.num q.den ⊆ rationalSubset Aplus T s), IsUnit ((ringHomOfRationalSubsetSubset P Aplus hAplus T s S hden q.num q.den (Localization.Away q.den) ⋯ hsub) f)

An element of A⟨T/s⟩ is nonzero at x exactly when it is a unit near x. Let R(T/s) be a rational subset of Spa (A, A⁺) with open numerator ideal and x ∈ R(T/s). Then f ∈ A⟨T/s⟩ lies outside the support of the point of Spa (A⟨T/s⟩, A_U⁺) over x if and only if there is a rational subset R(q) ⊆ R(T/s) containing x, presented by an admissible presentation q, such that the image of f in A⟨q⟩ is a unit.

theorem TauCeti.ValuationSpectrum.isUnit_toCompletionLoc_iff_forall_notMem_supp {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hP : P.ringOfDefinition ≤ Aplus) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (a : A) : IsUnit ((P.toCompletionLoc T s S hden) a) ↔ ∀ v ∈ rationalSubset Aplus T s, a ∉ v.supp

An element of A is invertible on R(T/s) exactly when its support misses that rational subset. This transfers the unit criterion for the complete Huber pair A⟨T/s⟩ across the homeomorphism of its spectrum with R(T/s).