English
There exists a valuation v on the fraction field K with value group ValueGroup(A,K), i.e., a map v: K → ValueGroup(A,K) satisfying the valuation axioms (v(xy)=v(x)v(y), v(x+y) ≤ max(v(x), v(y))).
Русский
Существует оценка v на дробном поле K, значение которой лежит в ValueGroup(A,K); то есть v: K → ValueGroup(A,K) удовлетворяет аксиомам оценки: v(xy)=v(x)v(y), v(x+y) ≤ max(v(x),v(y)).
LaTeX
$$$\\exists v:\\mathrm{Valuation}(K,\\mathrm{ValueGroup}(A,K)).$$$
Lean4
/-- Any valuation ring induces a valuation on its fraction field. -/
noncomputable def valuation : Valuation K (ValueGroup A K)
where
toFun := Quotient.mk''
map_zero' := rfl
map_one' := rfl
map_mul' _ _ := rfl
map_add_le_max' := by
intro a b
obtain ⟨xa, ya, hya, rfl⟩ : ∃ a b : A, _ := IsFractionRing.div_surjective a
obtain ⟨xb, yb, hyb, rfl⟩ : ∃ a b : A, _ := IsFractionRing.div_surjective b
have : (algebraMap A K) ya ≠ 0 := IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors hya
have : (algebraMap A K) yb ≠ 0 := IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors hyb
obtain ⟨c, h | h⟩ := ValuationRing.cond (xa * yb) (xb * ya)
· apply le_trans _ (le_max_left _ _)
use c + 1
rw [Algebra.smul_def]
field_simp
simp only [← RingHom.map_mul, ← RingHom.map_add]
congr 1; linear_combination h
· apply le_trans _ (le_max_right _ _)
use c + 1
rw [Algebra.smul_def]
field_simp
simp only [← RingHom.map_mul, ← RingHom.map_add]
congr 1; linear_combination h