The valuation spectrum of a ring

We define the valuation spectrum Spv A following Wedhorn, Adic Spaces (arXiv:1910.05934v1), Definition 4.1.

Main definitions

• TauCeti.ValuationSpectrum A : The valuation spectrum, the type of ValuativeRel instances on A.
• TauCeti.ValuationSpectrum.basicOpen f s : The basic open set {v ∈ Spv A | v(f) ≤ v(s) ≠ 0}.
• TauCeti.ValuationSpectrum.comap φ : The continuous map Spv B → Spv A induced by φ : A →+* B.
• TauCeti.ValuationSpectrum.supp v : The support ideal {a ∈ A | v(a) = 0}.
• TauCeti.ValuationSpectrum.basicOpenFinset_inter : Wedhorn's step (i) in the proof of Lemma 7.5, that the rational opens are stable under finite intersection.
• TauCeti.ValuationSpectrum.basicOpenFinset_image_mul_right : scaling every numerator and the denominator by a unit gives the same rational open.
• TauCeti.ValuationSpectrum.comap_preimage_basicOpenFinset : a rational open pulls back to the rational open presented by the images of its numerators and denominator.
• TauCeti.ValuationSpectrum.isClosed_setOfPred_forall_vlt_one : the sub-unit locus of a set of ring elements is closed — the closedness behind Wedhorn's Corollary 7.12.
• TauCeti.ValuationSpectrum.quotientLift 𝔞 h : Lift the implicitly inferred point v with 𝔞 ≤ supp v to Spv (A ⧸ 𝔞).
• TauCeti.ValuationSpectrum.localizationComapSection S B v hS : Lift v to a localization Spv B.
• TauCeti.ValuationSpectrum.localization_comap_isEmbedding : pullback from the valuation spectrum of a localization is a topological embedding.
• TauCeti.ValuationSpectrum.suppFun : The continuous support map Spv A → Spec A.
• TauCeti.ValuationSpectrum.trivialSection : The continuous section of suppFun given by the trivial valuation attached to a prime ideal; in particular suppFun is surjective (suppFun_surjective).

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Definition 4.1, Remark 4.3, Remark 4.4, Remark 4.6, Proposition 4.7(2)

Ported from the open Mathlib pull request leanprover-community/mathlib4#38009 (which supersedes an earlier draft in AINTLIB projects/AdicSpaces); this copy is deleted in favour of the Mathlib declarations once that pull request reaches the pinned Mathlib.

The localization embedding follows the organization and generated-topology argument of Mathlib's PrimeSpectrum.localization_comap_isEmbedding, adapted here from prime ideals to valuative relations.

structure TauCeti.ValuationSpectrum (A : Type u_1) [CommRing A] : Type u_1

The valuation spectrum Spv A of a commutative ring A. A point of Spv A is a ValuativeRel A, but Spv A is kept as a distinct type so it can carry its own topology without affecting ValuativeRel A.

• ofValuativeRel :: (
• toValuativeRel : ValuativeRel A

  The underlying ValuativeRel A of a point v : Spv A.

• )

theorem TauCeti.ValuationSpectrum.ext {A : Type u_1} {inst✝ : CommRing A} {x y : ValuationSpectrum A} (toValuativeRel : x.toValuativeRel = y.toValuativeRel) : x = y

theorem TauCeti.ValuationSpectrum.ext_iff {A : Type u_1} {inst✝ : CommRing A} {x y : ValuationSpectrum A} : x = y ↔ x.toValuativeRel = y.toValuativeRel

def TauCeti.termSpv : Lean.ParserDescr

The valuation spectrum Spv A of a commutative ring A. A point of Spv A is a ValuativeRel A, but Spv A is kept as a distinct type so it can carry its own topology without affecting ValuativeRel A.

Equations

• TauCeti.termSpv = Lean.ParserDescr.node `TauCeti.termSpv 1024 (Lean.ParserDescr.symbol "Spv")

instance TauCeti.instIsEmptyValuationSpectrumOfSubsingleton {A : Type u_1} [CommRing A] [Subsingleton A] : IsEmpty (ValuationSpectrum A)

Over a subsingleton ring, the valuation spectrum is empty.

theorem TauCeti.ValuationSpectrum.ext' {A : Type u_1} [CommRing A] {v₁ v₂ : ValuationSpectrum A} (h : ∀ (x y : A), x ≤ᵥ y ↔ x ≤ᵥ y) : v₁ = v₂

Two points of Spv A are equal as soon as their underlying vle relations agree.

def TauCeti.ValuationSpectrum.ofValuation {A : Type u_1} [CommRing A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation A Γ₀) : ValuationSpectrum A

Construct a point of Spv A from a valuation v : Valuation A Γ₀.

Equations

• TauCeti.ValuationSpectrum.ofValuation v = { toValuativeRel := ValuativeRel.ofValuation v }

theorem TauCeti.ValuationSpectrum.ofValuation_eq_of_isEquiv {A : Type u_1} [CommRing A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {Γ'₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ'₀] {v₁ : Valuation A Γ₀} {v₂ : Valuation A Γ'₀} (h : v₁.IsEquiv v₂) : ofValuation v₁ = ofValuation v₂

Two equivalent valuations define the same point of Spv A.

def TauCeti.ValuationSpectrum.basicOpen {A : Type u_1} [CommRing A] (f s : A) : Set (ValuationSpectrum A)

The basic open subset Spv(A)(f/s) = {v ∈ Spv A | v(f) ≤ v(s) ∧ v(s) ≠ 0}.

Equations

• TauCeti.ValuationSpectrum.basicOpen f s = {v : TauCeti.ValuationSpectrum A | f ≤ᵥ s ∧ ¬s ≤ᵥ 0}

@[simp]

theorem TauCeti.ValuationSpectrum.mem_basicOpen_iff {A : Type u_1} [CommRing A] (f s : A) (v : ValuationSpectrum A) : v ∈ basicOpen f s ↔ f ≤ᵥ s ∧ ¬s ≤ᵥ 0

Membership in the basic open subset Spv(A)(f/s), as a normal form.

theorem TauCeti.ValuationSpectrum.basicOpen_mul_subset {A : Type u_1} [CommRing A] (t f s : A) : basicOpen (t * f) (t * s) ⊆ basicOpen f s

Scaling numerator and denominator by t shrinks the basic open subset: Spv(A)(tf/ts) ⊆ Spv(A)(f/s).

theorem TauCeti.ValuationSpectrum.basicOpen_one {A : Type u_1} [CommRing A] : basicOpen 1 1 = Set.univ

The basic open subset for f = s = 1 is the whole spectrum: Spv(A)(1/1) = Spv A. Not @[simp]: basicOpen_one_right together with ValuativeRel.vle_refl already reduces the left-hand side, so a simp attribute here would be redundant (simpNF).

theorem TauCeti.ValuationSpectrum.basicOpen_self {A : Type u_1} [CommRing A] (s : A) : basicOpen s s = {v : ValuationSpectrum A | ¬s ≤ᵥ 0}

The basic open subset for f = s consists of the points where v(s) ≠ 0: Spv(A)(s/s) = {v ∈ Spv A | v(s) ≠ 0}.

@[simp]

theorem TauCeti.ValuationSpectrum.basicOpen_one_right {A : Type u_1} [CommRing A] (f : A) : basicOpen f 1 = {v : ValuationSpectrum A | f ≤ᵥ 1}

The basic open subset at denominator 1 needs no nonvanishing clause: Spv(A)(f/1) = {v ∈ Spv A | v(f) ≤ 1}.

@[instance_reducible]

instance TauCeti.ValuationSpectrum.instTopologicalSpace {A : Type u_1} [CommRing A] : TopologicalSpace (ValuationSpectrum A)

The topology on Spv A generated by the basic open sets basicOpen f s for f, s : A.

Equations

• TauCeti.ValuationSpectrum.instTopologicalSpace = TopologicalSpace.generateFrom {U : Set (TauCeti.ValuationSpectrum A) | ∃ (f : A) (s : A), U = TauCeti.ValuationSpectrum.basicOpen f s}

theorem TauCeti.ValuationSpectrum.isOpen_basicOpen {A : Type u_1} [CommRing A] (f s : A) : IsOpen (basicOpen f s)

Each basic open subset is open in Spv A.

theorem TauCeti.ValuationSpectrum.instTopologicalSpace_eq_generateFrom {A : Type u_1} [CommRing A] : instTopologicalSpace = TopologicalSpace.generateFrom {U : Set (ValuationSpectrum A) | ∃ (f : A) (s : A), U = basicOpen f s}

The topology of Spv A is generated by the basic opens (the defining equation of the instance).

theorem TauCeti.ValuationSpectrum.vle_iff_mem_basicOpen_or {A : Type u_1} [CommRing A] (v : ValuationSpectrum A) (f s : A) : f ≤ᵥ s ↔ v ∈ basicOpen f s ∨ v ∉ basicOpen s s ∧ v ∉ basicOpen f f

The valuative relation of a point is determined by its basic opens: v(f) ≤ v(s) holds iff v lies in basicOpen f s, or s and f both lie in the support — the latter being detected by the diagonal basic opens basicOpen s s and basicOpen f f.

theorem TauCeti.ValuationSpectrum.isClosed_setOfPred_forall_vlt_one {A : Type u_1} [CommRing A] (S : Set A) : IsClosed {v : ValuationSpectrum A | ∀ a ∈ S, a <ᵥ 1}

The sub-unit locus of a set of ring elements is closed: demanding v(a) < 1 at every a ∈ S cuts out a closed subset of Spv A. The complement is the union over a ∈ S of the basic opens Spv(A)(1/a) — the condition 1 ≤ v(a) already forces v(a) ≠ 0, so no separate nonvanishing clause survives.

This is the closedness underlying Wedhorn's Corollary 7.12: Theorem 7.10 describes Cont A inside Spv (A, IA) by exactly such conditions, so Cont A is the trace of a closed set.

instance TauCeti.ValuationSpectrum.instT0Space {A : Type u_1} [CommRing A] : T0Space (ValuationSpectrum A)

Spv A is T0: inseparable points agree on every basic open, hence carry the same valuative relation.

def TauCeti.ValuationSpectrum.comap {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] (φ : A →+* B) (v : ValuationSpectrum B) : ValuationSpectrum A

The contravariant map Spv B → Spv A induced by φ : A →+* B.

Equations

• TauCeti.ValuationSpectrum.comap φ v = { toValuativeRel := ValuativeRel.comap φ v.toValuativeRel }

@[simp]

theorem TauCeti.ValuationSpectrum.comap_vle {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] (φ : A →+* B) (v : ValuationSpectrum B) {a₁ a₂ : A} : (a₁ ≤ᵥ a₂) = (φ a₁ ≤ᵥ φ a₂)

The relation of a pulled-back point compares images under φ.

@[simp]

theorem TauCeti.ValuationSpectrum.comap_vlt {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] (φ : A →+* B) (v : ValuationSpectrum B) {a₁ a₂ : A} : (a₁ <ᵥ a₂) = (φ a₁ <ᵥ φ a₂)

The strict relation of a pulled-back point compares images under φ.

@[simp]

theorem TauCeti.ValuationSpectrum.comap_ofValuation {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] {Γ₀ : Type u_5} [LinearOrderedCommGroupWithZero Γ₀] (φ : A →+* B) (v : Valuation B Γ₀) : comap φ (ofValuation v) = ofValuation (Valuation.comap φ v)

comap is compatible with ofValuation.

theorem TauCeti.ValuationSpectrum.comap_preimage_basicOpen {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] (φ : A →+* B) (f s : A) : comap φ ⁻¹' basicOpen f s = basicOpen (φ f) (φ s)

The preimage of Spv(A)(f/s) under comap φ is Spv(B)(φ(f)/φ(s)).

theorem TauCeti.ValuationSpectrum.continuous_comap {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] (φ : A →+* B) : Continuous (comap φ)

comap φ is continuous.

@[simp]

theorem TauCeti.ValuationSpectrum.comap_id {A : Type u_2} [CommRing A] : comap (RingHom.id A) = id

comap of the identity is the identity.

@[simp]

theorem TauCeti.ValuationSpectrum.comap_comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing A] [CommRing B] [CommRing C] (φ : A →+* B) (ψ : B →+* C) : comap (ψ.comp φ) = comap φ ∘ comap ψ

comap is contravariantly functorial: comap (ψ ∘ φ) = comap φ ∘ comap ψ.

theorem TauCeti.ValuationSpectrum.comap_injective {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] {φ : A →+* B} (hφ : Function.Surjective ⇑φ) : Function.Injective (comap φ)

comap φ is injective when φ is surjective.

theorem TauCeti.ValuationSpectrum.comap_hom_comap_hom {X Y Z : CommRingCat} (φ : X ⟶ Y) (ψ : Y ⟶ Z) (w : ValuationSpectrum ↑Z) : comap (CommRingCat.Hom.hom φ) (comap (CommRingCat.Hom.hom ψ) w) = comap (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp φ ψ)) w

Pulling back along two composable morphisms of commutative rings is pulling back along their composite.

def TauCeti.ValuationSpectrum.supp {A : Type u_1} [CommRing A] (v : ValuationSpectrum A) : Ideal A

The support ideal {a ∈ A | v(a) = 0} of a point v : Spv A.

Equations

• v.supp = ValuativeRel.supp A

@[simp]

theorem TauCeti.ValuationSpectrum.mem_supp_iff {A : Type u_1} [CommRing A] (v : ValuationSpectrum A) (x : A) : x ∈ v.supp ↔ x ≤ᵥ 0

Membership in the support, as the relation v(x) ≤ v(0).

instance TauCeti.ValuationSpectrum.instIsPrimeSupp {A : Type u_1} [CommRing A] (v : ValuationSpectrum A) : v.supp.IsPrime

The support of a point v : Spv A is a prime ideal.

@[simp]

theorem TauCeti.ValuationSpectrum.vle_ofValuation {A : Type u_1} [CommRing A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation A Γ₀) (x y : A) : x ≤ᵥ y ↔ v x ≤ v y

(ofValuation v).vle x y ↔ v x ≤ v y.

@[simp]

theorem TauCeti.ValuationSpectrum.supp_ofValuation {A : Type u_1} [CommRing A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation A Γ₀) : (ofValuation v).supp = v.supp

The support of ofValuation v equals v.supp.

noncomputable def TauCeti.ValuationSpectrum.valuation {A : Type u_1} [CommRing A] (v : ValuationSpectrum A) : Valuation A (ValuativeRel.ValueGroupWithZero A)

The canonical valuation associated to a point v : Spv A.

Equations

• v.valuation = ValuativeRel.valuation A

theorem TauCeti.ValuationSpectrum.valuation_def {A : Type u_1} [CommRing A] (v : ValuationSpectrum A) : v.valuation = ValuativeRel.valuation A

v.valuation is ValuativeRel.valuation for the valuative relation of v.

The two sides are definitionally equal, but the definition of TauCeti.ValuationSpectrum.valuation is not exposed outside this module, so a downstream module cannot match v.valuation against Mathlib's ValuativeRel.valuation API without this equation. It exists to cross that module boundary, not to abbreviate.

@[simp]

theorem TauCeti.ValuationSpectrum.valuation_le_iff {A : Type u_1} [CommRing A] (v : ValuationSpectrum A) (x y : A) : v.valuation x ≤ v.valuation y ↔ x ≤ᵥ y

Comparison under the canonical valuation of a point is the point's valuative relation.

@[simp]

theorem TauCeti.ValuationSpectrum.valuation_lt_iff {A : Type u_1} [CommRing A] (v : ValuationSpectrum A) (x y : A) : v.valuation x < v.valuation y ↔ x <ᵥ y

Strict comparison under the canonical valuation of a point is the point's strict valuative relation — the strict sibling of valuation_le_iff, and the direct bridge between strict valuation inequalities and vlt hypotheses.

theorem TauCeti.ValuationSpectrum.supp_eq_valuation_supp {A : Type u_1} [CommRing A] (v : ValuationSpectrum A) : v.supp = v.valuation.supp

The support of v : Spv A equals the support of its canonical valuation.

theorem TauCeti.ValuationSpectrum.supp_comap {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] (φ : A →+* B) (v : ValuationSpectrum B) : (comap φ v).supp = Ideal.comap φ v.supp

The support of a pullback is the preimage of the support.

@[simp]

theorem TauCeti.ValuationSpectrum.ofValuation_valuation {A : Type u_1} [CommRing A] (v : ValuationSpectrum A) : ofValuation v.valuation = v

The canonical valuation gives back the same point of Spv.

theorem TauCeti.ValuationSpectrum.isEquiv_valuation_ofValuation {A : Type u_1} [CommRing A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (w : Valuation A Γ₀) : (ofValuation w).valuation.IsEquiv w

The canonical valuation of the point determined by w is equivalent to w.

theorem TauCeti.ValuationSpectrum.self_le_supp_comap {A : Type u_1} [CommRing A] (𝔞 : Ideal A) (w : ValuationSpectrum (A ⧸ 𝔞)) : 𝔞 ≤ (comap (Ideal.Quotient.mk 𝔞) w).supp

𝔞 ≤ supp(comap(mk 𝔞, w)) for all w : Spv (A ⧸ 𝔞).

noncomputable def TauCeti.ValuationSpectrum.quotientLift {A : Type u_1} [CommRing A] (𝔞 : Ideal A) ⦃v : ValuationSpectrum A⦄ (h : 𝔞 ≤ v.supp) : ValuationSpectrum (A ⧸ 𝔞)

Lift a point v ∈ Spv A with 𝔞 ≤ supp v to Spv (A ⧸ 𝔞).

Equations

• TauCeti.ValuationSpectrum.quotientLift 𝔞 h = TauCeti.ValuationSpectrum.ofValuation (v.valuation.onQuot ⋯)

@[simp]

theorem TauCeti.ValuationSpectrum.comap_quotientLift {A : Type u_1} [CommRing A] (𝔞 : Ideal A) ⦃v : ValuationSpectrum A⦄ (h : 𝔞 ≤ v.supp) : comap (Ideal.Quotient.mk 𝔞) (quotientLift 𝔞 h) = v

comap (mk 𝔞) (quotientLift 𝔞 h) = v.

@[simp]

theorem TauCeti.ValuationSpectrum.quotientLift_comap {A : Type u_1} [CommRing A] (𝔞 : Ideal A) (w : ValuationSpectrum (A ⧸ 𝔞)) : quotientLift 𝔞 ⋯ = w

quotientLift 𝔞 (self_le_supp_comap 𝔞 w) = w.

theorem TauCeti.ValuationSpectrum.quotientMk_comap_range {A : Type u_1} [CommRing A] (𝔞 : Ideal A) : Set.range (comap (Ideal.Quotient.mk 𝔞)) = {v : ValuationSpectrum A | 𝔞 ≤ v.supp}

The range of comap (mk 𝔞) is {v ∈ Spv A | 𝔞 ≤ supp v}.

theorem TauCeti.ValuationSpectrum.isEmbedding_comap_quotientMk {A : Type u_1} [CommRing A] (𝔞 : Ideal A) : Topology.IsEmbedding (comap (Ideal.Quotient.mk 𝔞))

comap (mk 𝔞) : Spv (A ⧸ 𝔞) → Spv A is a topological embedding.

noncomputable def TauCeti.ValuationSpectrum.localizationComapSection {A : Type u_1} [CommRing A] (S : Submonoid A) (B : Type u_2) [CommRing B] [Algebra A B] [IsLocalization S B] (v : ValuationSpectrum A) (hS : S ≤ v.supp.primeCompl) : ValuationSpectrum B

Send v ∈ Spv A with S ≤ (supp v).primeCompl to the localization Spv B, where B is a localization of A at the submonoid S.

Equations

• TauCeti.ValuationSpectrum.localizationComapSection S B v hS = TauCeti.ValuationSpectrum.ofValuation (v.valuation.extendToLocalization ⋯ B)

@[simp]

theorem TauCeti.ValuationSpectrum.comap_localizationComapSection {A : Type u_1} [CommRing A] (S : Submonoid A) (B : Type u_2) [CommRing B] [Algebra A B] [IsLocalization S B] (v : ValuationSpectrum A) (hS : S ≤ v.supp.primeCompl) : comap (algebraMap A B) (localizationComapSection S B v hS) = v

comap (algebraMap A B) (localizationComapSection S B v hS) = v.

theorem TauCeti.ValuationSpectrum.submonoid_le_supp_primeCompl_comap_algebraMap {A : Type u_1} [CommRing A] (S : Submonoid A) (B : Type u_2) [CommRing B] [Algebra A B] [IsLocalization S B] (w : ValuationSpectrum B) : S ≤ (comap (algebraMap A B) w).supp.primeCompl

S is disjoint from supp(comap(algebraMap, w)) for w : Spv B.

theorem TauCeti.ValuationSpectrum.localization_comap_range {A : Type u_1} [CommRing A] (S : Submonoid A) (B : Type u_2) [CommRing B] [Algebra A B] [IsLocalization S B] : Set.range (comap (algebraMap A B)) = {v : ValuationSpectrum A | S ≤ v.supp.primeCompl}

The range of comap (algebraMap A B) is {v | S ≤ supp(v).primeCompl}.

theorem TauCeti.ValuationSpectrum.localization_comap_injective {A : Type u_1} [CommRing A] (S : Submonoid A) (B : Type u_2) [CommRing B] [Algebra A B] [IsLocalization S B] : Function.Injective (comap (algebraMap A B))

Pullback of valuative relations along a localization map is injective.

theorem TauCeti.ValuationSpectrum.comap_preimage_basicOpen_mk' {A : Type u_1} [CommRing A] (S : Submonoid A) (B : Type u_2) [CommRing B] [Algebra A B] [IsLocalization S B] (a₁ a₂ : A) (s₁ s₂ : ↥S) : comap (algebraMap A B) ⁻¹' basicOpen (a₁ * ↑s₂) (a₂ * ↑s₁) = basicOpen (IsLocalization.mk' B a₁ s₁) (IsLocalization.mk' B a₂ s₂)

The preimage under localization pullback of the basic open obtained by clearing denominators is the basic open defined by the original fractions.

theorem TauCeti.ValuationSpectrum.localization_comap_isInducing {A : Type u_1} [CommRing A] (S : Submonoid A) (B : Type u_2) [CommRing B] [Algebra A B] [IsLocalization S B] : Topology.IsInducing (comap (algebraMap A B))

Pullback of valuative relations along a localization map induces the source topology.

theorem TauCeti.ValuationSpectrum.localization_comap_isEmbedding {A : Type u_1} [CommRing A] (S : Submonoid A) (B : Type u_2) [CommRing B] [Algebra A B] [IsLocalization S B] : Topology.IsEmbedding (comap (algebraMap A B))

Pullback of valuative relations along a localization map is a topological embedding.

The support map to the prime spectrum

def TauCeti.ValuationSpectrum.suppFun {A : Type u_1} [CommRing A] : ValuationSpectrum A → PrimeSpectrum A

The support map Spv A → Spec A.

Equations

• v.suppFun = { asIdeal := v.supp, isPrime := ⋯ }

@[simp]

theorem TauCeti.ValuationSpectrum.suppFun_asIdeal {A : Type u_1} [CommRing A] (v : ValuationSpectrum A) : v.suppFun.asIdeal = v.supp

The prime ideal underlying suppFun v is the support of v.

theorem TauCeti.ValuationSpectrum.suppFun_preimage_basicOpen {A : Type u_1} [CommRing A] (f : A) : suppFun ⁻¹' ↑(PrimeSpectrum.basicOpen f) = basicOpen f f

suppFun ⁻¹' D(f) = Spv(A)(f/f).

theorem TauCeti.ValuationSpectrum.continuous_suppFun {A : Type u_1} [CommRing A] : Continuous suppFun

suppFun is continuous.

theorem TauCeti.ValuationSpectrum.suppFun_comap {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] (φ : A →+* B) (v : ValuationSpectrum B) : (comap φ v).suppFun = PrimeSpectrum.comap φ v.suppFun

supp ∘ Spv(φ) = Spec(φ) ∘ supp.

The trivial-valuation section of the support map

noncomputable def TauCeti.ValuationSpectrum.trivialSection {A : Type u_1} [CommRing A] (p : PrimeSpectrum A) : ValuationSpectrum A

The trivial-valuation section of the support map (Wedhorn, Remark 4.6): the point of Spv A given by the trivial valuation attached to a prime ideal.

Equations

• TauCeti.ValuationSpectrum.trivialSection p = TauCeti.ValuationSpectrum.ofValuation (Valuation.trivialValuation p.asIdeal)

@[simp]

theorem TauCeti.ValuationSpectrum.trivialSection_vle_iff {A : Type u_1} [CommRing A] (p : PrimeSpectrum A) (f s : A) : f ≤ᵥ s ↔ f ∈ p.asIdeal ∨ s ∉ p.asIdeal

The valuative relation of a trivial-valuation point: v(f) ≤ v(s) holds precisely when f lies in the prime or s does not.

@[simp]

theorem TauCeti.ValuationSpectrum.suppFun_trivialSection {A : Type u_1} [CommRing A] (p : PrimeSpectrum A) : (trivialSection p).suppFun = p

trivialSection is a section of the support map.

theorem TauCeti.ValuationSpectrum.trivialSection_preimage_basicOpen {A : Type u_1} [CommRing A] (f s : A) : trivialSection ⁻¹' basicOpen f s = ↑(PrimeSpectrum.basicOpen s)

The preimage of a basic open under trivialSection is the corresponding basic open of the prime spectrum: trivialSection ⁻¹' Spv(A)(f/s) = D(s).

theorem TauCeti.ValuationSpectrum.continuous_trivialSection {A : Type u_1} [CommRing A] : Continuous trivialSection

trivialSection is continuous.

theorem TauCeti.ValuationSpectrum.suppFun_surjective {A : Type u_1} [CommRing A] : Function.Surjective suppFun

The support map is surjective; the trivial valuations provide a section.

Rational opens with a finite numerator set

def TauCeti.ValuationSpectrum.basicOpenFinset {A : Type u_1} [CommRing A] (T : Finset A) (s : A) : Set (ValuationSpectrum A)

Wedhorn's Spv(A)(T/s) for a finite set T: the points where every t ∈ T is dominated by s, and s is not in the support.

Equations

• TauCeti.ValuationSpectrum.basicOpenFinset T s = {v : TauCeti.ValuationSpectrum A | (∀ t ∈ T, t ≤ᵥ s) ∧ ¬s ≤ᵥ 0}

@[simp]

theorem TauCeti.ValuationSpectrum.mem_basicOpenFinset_iff {A : Type u_1} [CommRing A] (T : Finset A) (s : A) (v : ValuationSpectrum A) : v ∈ basicOpenFinset T s ↔ (∀ t ∈ T, t ≤ᵥ s) ∧ ¬s ≤ᵥ 0

theorem TauCeti.ValuationSpectrum.basicOpenFinset_subset_basicOpen {A : Type u_1} [CommRing A] {T : Finset A} {s t : A} (ht : t ∈ T) : basicOpenFinset T s ⊆ basicOpen t s

Each numerator gives back an ordinary basic open.

theorem TauCeti.ValuationSpectrum.basicOpenFinset_eq_biInter {A : Type u_1} [CommRing A] (T : Finset A) (s : A) : basicOpenFinset T s = ⋂ t ∈ insert s ↑T, basicOpen t s

Spv(A)(T/s) is the finite intersection of the basic opens Spv(A)(t/s) for t ranging over T ∪ {s}; the extra s is what carries the nonvanishing clause when T is empty.

theorem TauCeti.ValuationSpectrum.isOpen_basicOpenFinset {A : Type u_1} [CommRing A] (T : Finset A) (s : A) : IsOpen (basicOpenFinset T s)

@[simp]

theorem TauCeti.ValuationSpectrum.basicOpenFinset_insert_self {A : Type u_1} [CommRing A] (T : Finset A) (s : A) : basicOpenFinset (insert s T) s = basicOpenFinset T s

Inserting the denominator among the numerators changes nothing: the extra condition it adds is v s ≤ v s.

@[simp]

theorem TauCeti.ValuationSpectrum.basicOpenFinset_image_mul_right {A : Type u_1} [CommRing A] (T : Finset A) (s u : A) (hu : IsUnit u) : basicOpenFinset (Finset.image (fun (t : A) => t * u) T) (s * u) = basicOpenFinset T s

Multiplying a presentation by a unit changes nothing. If u is a unit, then multiplying every numerator and the denominator of Spv(A)(T/s) by u gives the same rational open.

No injectivity of t ↦ t * u is needed.

theorem TauCeti.ValuationSpectrum.comap_preimage_basicOpenFinset {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] (φ : A →+* B) (T : Finset A) (s : A) : comap φ ⁻¹' basicOpenFinset T s = basicOpenFinset (Finset.image (⇑φ) T) (φ s)

The preimage of Spv(A)(T/s) under comap φ is Spv(B)(φ(T)/φ(s)), the finite-numerator form of comap_preimage_basicOpen.

@[simp]

theorem TauCeti.ValuationSpectrum.basicOpenFinset_inter {A : Type u_1} [CommRing A] (T₁ T₂ : Finset A) (s₁ s₂ : A) : basicOpenFinset T₁ s₁ ∩ basicOpenFinset T₂ s₂ = basicOpenFinset (insert s₁ T₁ * insert s₂ T₂) (s₁ * s₂)

Wedhorn's step (i) in the proof of Lemma 7.5: the rational opens are stable under finite intersection. Writing Uᵢ = insert sᵢ Tᵢ for the numerator set augmented by its own denominator,

Spv(A)(T₁/s₁) ∩ Spv(A)(T₂/s₂) = Spv(A)(U₁U₂ / s₁s₂).

The numerator sets on the right carry their own denominators, which basicOpenFinset_insert_self shows costs nothing — the same absorption IsAdmissible performs for the admissibility condition.