The valuation on a stalk of the presentation-limit presheaf

Let x be a point of X = Spa(A,A⁺). Every rational neighbourhood R(p) of x has coordinate ring A⟨p⟩, and x determines a point of Spa (A⟨p⟩, A_p⁺) through the homeomorphism Spa (A⟨p⟩, A_p⁺) ≃ₜ R(p) of Wedhorn's Proposition 8.2(2). This file glues these points along the germ maps into a point of the valuation spectrum of the presentation-limit presheaf stalk. It is the presheaf-stalk version of the valuation v_x which Wedhorn attaches to x in §8.1. No comparison with the adic-space structure sheaf is established here.

The gluing is TauCeti.ValuationSpectrum.ofDirected. Its hypotheses are supplied here: every germ is the germ of an element of some A⟨p⟩; a germ vanishes only if some restriction to a smaller rational neighbourhood does. The compatibility of the points of x on the rings A⟨p⟩ with the comparison maps of Wedhorn's Proposition 8.2(1) comes from Spa.Localization.Point. Two lifts of one germ therefore differ, on a common rational neighbourhood, by an element of the support of the point of x, and so they have the same value.

The stalk is the ring colimit of presentationLimitPresheafInCommRingCat; no topology on it is used. A⁺ is assumed to consist of power-bounded elements, as for every ring of integral elements, and to contain the ring of definition of the chosen pair of definition, as spaCompletedLocalizationHomeomorph requires.

Main definitions

• TauCeti.ValuationSpectrum.presentationLimitStalkValuation: the valuation on the stalk at x.

Main results

• TauCeti.ValuationSpectrum.comap_presentationLimitRationalGerm_presentationLimitStalkValuation: pulled back along the germ map of a rational neighbourhood R(p), the stalk valuation is the point of A⟨p⟩ determined by x.
• TauCeti.ValuationSpectrum.eq_presentationLimitStalkValuation: it is the only point of the valuation spectrum of the stalk with this property.
• TauCeti.ValuationSpectrum.comap_presentationLimitStalkValuation: pulled back to A, the stalk valuation is x itself.

References

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

The stalk valuation

noncomputable def TauCeti.ValuationSpectrum.presentationLimitStalkValuation {A : Type v} [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) (x : ↑(spa Aplus)) : ValuationSpectrum ↑((presentationLimitPresheafInCommRingCat P Aplus).stalk x)

The valuation on the stalk of the presentation-limit presheaf at a point x of Spa(A,A⁺): the point of its valuation spectrum which, on the germs of every rational neighbourhood R(p) of x, is the point of A⟨p⟩ that x determines under Spa (A⟨p⟩, A_p⁺) ≃ₜ R(p).

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.ValuationSpectrum.comap_presentationLimitRationalGerm_presentationLimitStalkValuation {A : Type v} [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) (p : P.Presentation) (hp : IsOpen ↑(Ideal.span ↑p.num)) (x : ↑(spa Aplus)) (hx : x ∈ spaBasicOpen Aplus p.num p.den) : comap (CommRingCat.Hom.hom (presentationLimitRationalGerm hAplus p hp x hx)) (presentationLimitStalkValuation hAplus hP x) = rationalLocalizationPoint hP p x hx

The stalk valuation restricts to the rational points: its pullback along the germ map of a rational neighbourhood R(p) of x is the point of A⟨p⟩ determined by x. Not @[simp]: presentationLimitRationalGerm_def simplifies the left-hand side first.

theorem TauCeti.ValuationSpectrum.eq_presentationLimitStalkValuation {A : Type v} [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) {x : ↑(spa Aplus)} {v : ValuationSpectrum ↑((presentationLimitPresheafInCommRingCat P Aplus).stalk x)} (hv : ∀ (p : P.Presentation) (hp : IsOpen ↑(Ideal.span ↑p.num)) (hx : x ∈ spaBasicOpen Aplus p.num p.den), comap (CommRingCat.Hom.hom (presentationLimitRationalGerm hAplus p hp x hx)) v = rationalLocalizationPoint hP p x hx) : v = presentationLimitStalkValuation hAplus hP x

Uniqueness of the stalk valuation: a point of the valuation spectrum of the stalk at x whose pullback along the germ map of every rational neighbourhood R(p) of x is the point of A⟨p⟩ determined by x is presentationLimitStalkValuation.

theorem TauCeti.ValuationSpectrum.comap_presentationLimitStalkValuation {A : Type v} [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) (p : P.Presentation) (hp : IsOpen ↑(Ideal.span ↑p.num)) (x : ↑(spa Aplus)) (hx : x ∈ spaBasicOpen Aplus p.num p.den) : comap (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (P.toCompletionLoc p.num p.den (Localization.Away p.den) ⋯)) (CategoryTheory.CategoryStruct.comp p.completionLocObjCommRingCatIso.inv (presentationLimitRationalGerm hAplus p hp x hx)))) (presentationLimitStalkValuation hAplus hP x) = ↑x

The stalk valuation lies over x: pulled back to A along the structure map A → A⟨p⟩ and the germ map of a rational neighbourhood R(p) of x, the stalk valuation at x is x. Not @[simp]: comap_comp and presentationLimitRationalGerm_def simplify the left-hand side first.