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 ≤ Ideal.primeCompl (Valuation.supp v))
(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.
Equations
- One or more equations did not get rendered due to their size.
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 ≤ Ideal.primeCompl (Valuation.supp v))
(B : Type u_3)
[CommRing B]
[Algebra A B]
[IsLocalization S B]
(a : A)
:
(Valuation.extendToLocalization v hS B) ((algebraMap A B) a) = v a