English
If R is maximal (dup), there exists a valuation subring giving R as its local subring.
Русский
Если R максимальное (повтор), существует valuationSubring, дающее R как локальное подкольцо.
LaTeX
$$$\\exists B:\\mathrm{ValuationSubring}(K), \\; B^{\\mathrm{toLocalSubring}} = R.$$$
Lean4
/-- If `hJ : J ⊆ supp v` then `onQuotVal hJ` is the induced function on `R / J` as a function.
Note: it's just the function; the valuation is `onQuot hJ`. -/
def onQuotVal {J : Ideal R} (hJ : J ≤ supp v) : R ⧸ J → Γ₀ := fun q =>
Quotient.liftOn' q v fun a b h =>
calc
v a = v (b + -(-a + b)) := by simp
_ = v b := v.map_add_supp b <| (Ideal.neg_mem_iff _).2 <| hJ <| QuotientAddGroup.leftRel_apply.mp h
