Extending valuations to a localization

We show that, given a valuation v taking values in a linearly ordered commutative group with zero Γ, and a submonoid S of v.supp.primeCompl, the valuation v can be naturally extended to the localization S⁻¹A.

noncomputable def Valuation.extendToLocalization {A : Type u_1} [CommRing A] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] (v : Valuation A Γ) {S : Submonoid A} (hS : S ≤ v.supp.primeCompl) (B : Type u_3) [CommRing B] [Algebra A B] [IsLocalization S B] : Valuation B Γ

We can extend a valuation v on a ring to a localization at a submonoid of the complement of v.supp.

Equations

• v.extendToLocalization hS B = { toFun := (↑((IsLocalization.toLocalizationMap S B).lift ⋯)).toFun, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }

@[simp]

theorem Valuation.extendToLocalization_apply_map_apply {A : Type u_1} [CommRing A] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] (v : Valuation A Γ) {S : Submonoid A} (hS : S ≤ v.supp.primeCompl) (B : Type u_3) [CommRing B] [Algebra A B] [IsLocalization S B] (a : A) : (v.extendToLocalization hS B) ((algebraMap A B) a) = v a