Points of the valuation spectrum of a directed union of images

Let R be a commutative ring and fᵢ : Bᵢ → R a family of ring homomorphisms whose images form a directed family of subrings covering R, as for the canonical maps into a filtered colimit of rings. A family of points wᵢ ∈ Spv Bᵢ that is compatible in the sense that

fᵢ a = fⱼ a',  fᵢ b = fⱼ b',  a ≤_{wᵢ} b   ⟹   a' ≤_{wⱼ} b'

glues to a unique point w ∈ Spv R whose pullback along each fᵢ is wᵢ: to compare two elements of R, lift both to a common Bᵢ and compare the lifts with wᵢ.

This is how a valuation on a stalk is assembled from valuations on the rings of sections over the neighbourhoods of a point.

Main definitions

• TauCeti.ValuationSpectrum.ofDirected: the glued point of Spv R.

Main results

• TauCeti.ValuationSpectrum.vle_ofDirected_iff: two elements lifted to a common Bᵢ compare as their lifts do for wᵢ.
• TauCeti.ValuationSpectrum.comap_ofDirected: the glued point pulls back to wᵢ along fᵢ.
• TauCeti.ValuationSpectrum.eq_ofDirected: it is the only point of Spv R with this property.

noncomputable def TauCeti.ValuationSpectrum.ofDirected {R : Type u_1} [CommRing R] {ι : Type u_2} {B : ι → Type u_3} [(i : ι) → CommRing (B i)] (f : (i : ι) → B i →+* R) {w : (i : ι) → ValuationSpectrum (B i)} (hcompat : ∀ (i j : ι) (a b : B i) (a' b' : B j), (f i) a = (f j) a' → (f i) b = (f j) b' → a ≤ᵥ b → a' ≤ᵥ b') (hdir : Directed (fun (x1 x2 : Subring R) => x1 ≤ x2) fun (i : ι) => (f i).range) (hcover : ∀ (r : R), ∃ (i : ι), r ∈ (f i).range) : ValuationSpectrum R

The point glued from a compatible family on a directed union of images. Two elements of R are compared by lifting them to a common Bᵢ and comparing the lifts with wᵢ; the compatibility hypothesis makes the answer independent of the lifts.

Equations

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

theorem TauCeti.ValuationSpectrum.vle_ofDirected_iff {R : Type u_1} [CommRing R] {ι : Type u_2} {B : ι → Type u_3} [(i : ι) → CommRing (B i)] (f : (i : ι) → B i →+* R) {w : (i : ι) → ValuationSpectrum (B i)} (hcompat : ∀ (i j : ι) (a b : B i) (a' b' : B j), (f i) a = (f j) a' → (f i) b = (f j) b' → a ≤ᵥ b → a' ≤ᵥ b') (hdir : Directed (fun (x1 x2 : Subring R) => x1 ≤ x2) fun (i : ι) => (f i).range) (hcover : ∀ (r : R), ∃ (i : ι), r ∈ (f i).range) {i : ι} {a b : B i} {r s : R} (ha : (f i) a = r) (hb : (f i) b = s) : r ≤ᵥ s ↔ a ≤ᵥ b

Comparison in the glued point of two elements lifted to a common Bᵢ is comparison of the lifts for wᵢ.

@[simp]

theorem TauCeti.ValuationSpectrum.comap_ofDirected {R : Type u_1} [CommRing R] {ι : Type u_2} {B : ι → Type u_3} [(i : ι) → CommRing (B i)] (f : (i : ι) → B i →+* R) {w : (i : ι) → ValuationSpectrum (B i)} (hcompat : ∀ (i j : ι) (a b : B i) (a' b' : B j), (f i) a = (f j) a' → (f i) b = (f j) b' → a ≤ᵥ b → a' ≤ᵥ b') (hdir : Directed (fun (x1 x2 : Subring R) => x1 ≤ x2) fun (i : ι) => (f i).range) (hcover : ∀ (r : R), ∃ (i : ι), r ∈ (f i).range) (i : ι) : comap (f i) (ofDirected f hcompat hdir hcover) = w i

The glued point restricts to the given points: its pullback along fᵢ is wᵢ.

theorem TauCeti.ValuationSpectrum.eq_ofDirected {R : Type u_1} [CommRing R] {ι : Type u_2} {B : ι → Type u_3} [(i : ι) → CommRing (B i)] (f : (i : ι) → B i →+* R) {w : (i : ι) → ValuationSpectrum (B i)} (hcompat : ∀ (i j : ι) (a b : B i) (a' b' : B j), (f i) a = (f j) a' → (f i) b = (f j) b' → a ≤ᵥ b → a' ≤ᵥ b') (hdir : Directed (fun (x1 x2 : Subring R) => x1 ≤ x2) fun (i : ι) => (f i).range) (hcover : ∀ (r : R), ∃ (i : ι), r ∈ (f i).range) {v : ValuationSpectrum R} (hv : ∀ (i : ι), comap (f i) v = w i) : v = ofDirected f hcompat hdir hcover

Uniqueness of the glued point: a point of Spv R whose pullback along every fᵢ is wᵢ is ofDirected.