Documentation

Mathlib.RingTheory.Valuation.ExtendToLocalization

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] :

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' := }
Instances For
    @[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