English
The map on value groups commutes with valuation: mapValueGroupWithZero (valuation a) equals valuation (algebraMap a).
Русский
Отображение значений согласуется с оценкой: mapValueGroupWithZero (valuation a) = valuation (algebraMap a).
LaTeX
$$$\\mathrm{mapValueGroupWithZero}(A,B)(\\mathrm{valuation}(a)) = \\mathrm{valuation}(\\mathrm{algebraMap}(A,B)(a))$$$
Lean4
/-- Any valuation compatible with the valuative relation can be factored through
the value group. -/
noncomputable def embed [h : v.Compatible] : ValueGroupWithZero R →*₀ Γ
where
toFun :=
ValuativeRel.ValueGroupWithZero.lift (fun r s ↦ v r / v (s : R)) <|
by
intro x y r s
simp only [h.rel_iff_le, map_mul, ← and_imp, ← le_antisymm_iff]
rw [div_eq_div_iff] <;> simp
map_zero' := by simp [ValueGroupWithZero.lift_zero]
map_one' := by simp
map_mul' _
_ := by
apply ValuativeRel.ValueGroupWithZero.lift_mul
simp [field]
