valuation — Mathlib

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

Похожие утверждения