Points on completed rational localizations

A point of a rational subset of Spa(A,A⁺) determines a point of its completed rational localization through Wedhorn's Proposition 8.2(2). These points agree along the comparison maps of Proposition 8.2(1).

Main definitions

• TauCeti.ValuationSpectrum.rationalLocalizationPoint: the point of A⟨p⟩ determined by x ∈ R(p).

Main results

• TauCeti.ValuationSpectrum.rationalLocalizationPoint_def: the defining formula.
• TauCeti.ValuationSpectrum.comap_rationalLocalizationPoint: the rational point lies over x.
• TauCeti.ValuationSpectrum.comap_homOfRationalSubsetSubset_rationalLocalizationPoint: the rational points agree along comparison maps.

noncomputable def TauCeti.ValuationSpectrum.rationalLocalizationPoint {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hP : P.ringOfDefinition ≤ Aplus) (p : P.Presentation) (x : ↑(spa Aplus)) (hx : x ∈ spaBasicOpen Aplus p.num p.den) : ValuationSpectrum ↑((TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat)).obj p.completionLocObj)

The point of the rational coordinate ring A⟨p⟩ determined by a point x of the rational subset R(p): the preimage of x under the homeomorphism Spa (A⟨p⟩, A_p⁺) ≃ₜ R(p) of Wedhorn's Proposition 8.2(2), read on the underlying ring of p.completionLocObj.

Equations

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

theorem TauCeti.ValuationSpectrum.rationalLocalizationPoint_def {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hP : P.ringOfDefinition ≤ Aplus) (p : P.Presentation) (x : ↑(spa Aplus)) (hx : x ∈ spaBasicOpen Aplus p.num p.den) : rationalLocalizationPoint hP p x hx = comap (CommRingCat.Hom.hom p.completionLocObjCommRingCatIso.hom) ↑((spaCompletedLocalizationHomeomorph P Aplus hP p.num p.den (Localization.Away p.den) ⋯).symm ⟨x, ⋯⟩)

The point of A⟨p⟩ determined by x ∈ R(p) is the preimage of x under spaCompletedLocalizationHomeomorph, pulled back along completionLocObjCommRingCatIso.

@[simp]

theorem TauCeti.ValuationSpectrum.comap_rationalLocalizationPoint {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hP : P.ringOfDefinition ≤ Aplus) (p : P.Presentation) (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.forget₂ TopCommRingCat CommRingCat).map (CategoryTheory.eqToHom ⋯)))) (rationalLocalizationPoint hP p x hx) = ↑x

The rational point lies over x: pulled back along the structure map A → A⟨p⟩, the point of A⟨p⟩ determined by x ∈ R(p) is x itself.

@[simp]

theorem TauCeti.ValuationSpectrum.comap_homOfRationalSubsetSubset_rationalLocalizationPoint {A : Type v} [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) (p q : P.Presentation) (h : spaBasicOpen Aplus q.num q.den ≤ spaBasicOpen Aplus p.num p.den) (x : ↑(spa Aplus)) (hx : x ∈ spaBasicOpen Aplus q.num q.den) : comap (CommRingCat.Hom.hom ((CategoryTheory.forget₂ TopCommRingCat CommRingCat).map (homOfRationalSubsetSubset Aplus hAplus ⋯).hom)) (rationalLocalizationPoint hP q x hx) = rationalLocalizationPoint hP p x ⋯

The rational points are compatible with the comparison maps: for a containment R(q) ⊆ R(p) and x ∈ R(q), the comparison map A⟨p⟩ → A⟨q⟩ pulls the point of A⟨q⟩ determined by x back to the point of A⟨p⟩ determined by x.