mathlib3 documentation

ring_theory.valuation.extend_to_localization

Extending valuations to a localization #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} [linear_ordered_comm_group_with_zero Γ] (v : valuation A Γ) {S : submonoid A} (hS : S v.supp.prime_compl) (B : Type u_3) [comm_ring B] [algebra A B] [is_localization S 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} [linear_ordered_comm_group_with_zero Γ] (v : valuation A Γ) {S : submonoid A} (hS : S v.supp.prime_compl) (B : Type u_3) [comm_ring B] [algebra A B] [is_localization S B] (a : A) :