English
Let f: S → R be a ring homomorphism and let v be an AddValuation on R with value group Γ₀. Then the pullback of v along f is an AddValuation on S with the same value group, defined by (comap_f v)(s) = v(f(s)).
Русский
Пусть f: S → R — кольцевой гомоморфизм, пусть v — AddValuation на R с группой значений Γ₀. Тогда вытяжка v по f задаёт AddValuation на S той же группы значений, определяемую формулой (comap_f v)(s) = v(f(s)).
LaTeX
$$$$ \\mathrm{comap}_f : \\mathrm{AddValuation}(R, \\Gamma_0) \\to \\mathrm{AddValuation}(S, \\Gamma_0), \\quad (\\mathrm{comap}_f v)(s) = v(f(s)). $$$$
Lean4
/-- A ring homomorphism `S → R` induces a map `AddValuation R Γ₀ → AddValuation S Γ₀`. -/
def comap {S : Type*} [Ring S] (f : S →+* R) (v : AddValuation R Γ₀) : AddValuation S Γ₀ :=
Valuation.comap f v
