English
Let f: Γ₀ →+ Γ'₀ be a monotone, top-preserving monoid homomorphism. Then there is a map v ↦ v.map f ht hf from AddValuation R Γ₀ to AddValuation R Γ'₀, pushing forward the values along f.
Русский
Пусть f: Γ₀ →+ Γ'₀ — моноидовый гомоморфизм, сохраняющий верхнюю границу. Тогда существует отображение v ↦ v.map f ht hf от AddValuation R Γ₀ к AddValuation R Γ'₀, перенаправляющее значения через f.
LaTeX
$$$$ \\mathrm{map} : (f : Γ_0 \\to_+ Γ'_0) \\to \\bigl(AddValuation\\,R\\,Γ_0 \\to AddValuation\\,R\\,Γ'_0\\bigr), \\quad v \\mapsto v.map_f, $$\nwhere (v.map_f)(r) = f(v(r)) .$$$$
Lean4
/-- A `≤`-preserving, `⊤`-preserving group homomorphism `Γ₀ → Γ'₀` induces a map
`AddValuation R Γ₀ → AddValuation R Γ'₀`.
-/
def map (f : Γ₀ →+ Γ'₀) (ht : f ⊤ = ⊤) (hf : Monotone f) (v : AddValuation R Γ₀) : AddValuation R Γ'₀ :=
@Valuation.map R (Multiplicative Γ₀ᵒᵈ) (Multiplicative Γ'₀ᵒᵈ) _ _ _
{ toFun := f
map_mul' := f.map_add
map_one' := f.map_zero
map_zero' := ht } (fun _ _ h => hf h) v
