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] :
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.extend_to_localization hS B = let f : S.localization_map B := is_localization.to_localization_map S B, h : ∀ (s : ↥S), is_unit (⇑(v.to_monoid_with_zero_hom.to_monoid_hom) ↑s) := _ in {to_monoid_with_zero_hom := {to_fun := (f.lift h).to_fun, map_zero' := _, map_one' := _, map_mul' := _}, map_add_le_max' := _}
@[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) :
⇑(v.extend_to_localization hS B) (⇑(algebra_map A B) a) = ⇑v a