English
Let f: Γ0 →*₀ Γ'0 be a monotone monoid-with-zero homomorphism. Then, for any valuation v on R with values in Γ0, there is an induced valuation on R with values in Γ'0, defined by (v.map f hf)(r) = f(v(r)).
Русский
Пусть f: Γ0 →*₀ Γ'0 задан как монотонное отображение между моногруппами с нулем. Тогда для любой оценки v на R со значениями в Γ0 существует индуцированная оценка на R со значениями в Γ'0, заданная (v.map f hf)(r) = f(v(r)).
LaTeX
$$$\\forall f : Γ_0 \\to_*_0 Γ'_0\\, (hf : Monotone f)\\, (v : Valuation\\ R \\ Γ_0),\\; Valuation R Γ'_0$$
Lean4
/-- A `≤`-preserving group homomorphism `Γ₀ → Γ'₀` induces a map `Valuation R Γ₀ → Valuation R Γ'₀`.
-/
def map (f : Γ₀ →*₀ Γ'₀) (hf : Monotone f) (v : Valuation R Γ₀) : Valuation R Γ'₀ :=
{ MonoidWithZeroHom.comp f v.toMonoidWithZeroHom with
toFun := f ∘ v
map_add_le_max' := fun r s =>
calc
f (v (r + s)) ≤ f (max (v r) (v s)) := hf (v.map_add r s)
_ = max (f (v r)) (f (v s)) := hf.map_max }
