English
There exists a valuation on a localization B of A at S, extending the valuation v on A, provided S lies in the complement of the valuation's support and suitable localization data are given.
Русский
Существует оценка на локализацию B = S^{-1}A, которая расширяет v на A при условии, что S лежит в комплементарном множестве поддержки оценки и даны подходящие данные локализации.
LaTeX
$$$ \\exists \\tilde v:\\ Valuation\\ B\\ Γ \\text{ extending } v\\text{, given } S \\le v.supp.primeCompl. $$$
Lean4
/-- The ring isomorphism between a DVR `A` and the valuation subring of a field of fractions
of `A` endowed with the adic valuation of the maximal ideal. -/
noncomputable def equivValuationSubring : A ≃+* ((maximalIdeal A).valuation K).valuationSubring :=
(topEquiv.symm.trans (equivMapOfInjective ⊤ (algebraMap A K) (IsFractionRing.injective A _))).trans
(RingEquiv.subringCongr map_algebraMap_eq_valuationSubring)
