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.

@[simp]

theorem Valuation.extendToLocalization_mk' {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] (x : A) (y : ↥S) : (v.extendToLocalization hS B) (IsLocalization.mk' B x y) = v x * (v ↑y)⁻¹

@[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