mathlibdocumentation

ring_theory.valuation.extend_to_localization

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.prime_compl, the valuation v can be naturally extended to the localization S⁻¹A.

noncomputable def valuation.extend_to_localization {A : Type u_1} [comm_ring A] {Γ : Type u_2} (v : Γ) {S : submonoid A} (hS : S v.supp.prime_compl) (B : Type u_3) [comm_ring B] [ B] [ B] :
Γ

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

Equations
@[simp]
theorem valuation.extend_to_localization_apply_map_apply {A : Type u_1} [comm_ring A] {Γ : Type u_2} (v : Γ) {S : submonoid A} (hS : S v.supp.prime_compl) (B : Type u_3) [comm_ring B] [ B] [ B] (a : A) :
B) ( B) a) = v a