English
Equivalence of valuations is preserved under mapping by a monotone, injective monoid homomorphism.
Русский
Эквивалентность оценок сохраняется при отображении монотонным инъективным гомоморфизмом моноида.
LaTeX
$$$ (v \IsEquiv v') \rightarrow (v.map f \IsEquiv v'.map f) $, при условии, что f монотонен и инъективен.$$
Lean4
theorem map {v' : Valuation R Γ₀} (f : Γ₀ →*₀ Γ'₀) (hf : Monotone f) (inf : Injective f) (h : v.IsEquiv v') :
(v.map f hf).IsEquiv (v'.map f hf) :=
let H : StrictMono f := hf.strictMono_of_injective inf
fun r s =>
calc
f (v r) ≤ f (v s) ↔ v r ≤ v s := by rw [H.le_iff_le]
_ ↔ v' r ≤ v' s := (h r s)
_ ↔ f (v' r) ≤ f (v' s) := by rw [H.le_iff_le]
