English
The extendToLocalization construction provides a valuation on the localization B extending the valuation on A, compatible with the localization map.
Русский
Конструкция extendToLocalization даёт оценку на локализацию B, которая расширяет оценку на A и совместима с отображением локализации.
LaTeX
$$$ \\text{ExtendToLocalization }(v,hS,B) : Valuation\\ B \\Gamma \\text{ extending } v. $$$
Lean4
/-- We can extend a valuation `v` on a ring to a localization at a submonoid of
the complement of `v.supp`. -/
noncomputable def extendToLocalization : Valuation B Γ :=
let f := IsLocalization.toLocalizationMap S B
let h : ∀ s : S, IsUnit (v.1.toMonoidHom s) := fun s => isUnit_iff_ne_zero.2 (hS s.2)
{ f.lift h with
map_zero' := by convert f.lift_eq (P := Γ) _ 0 <;> simp [f]
map_add_le_max' := fun x y =>
by
obtain ⟨a, b, s, rfl, rfl⟩ : ∃ (a b : A) (s : S), f.mk' a s = x ∧ f.mk' b s = y :=
by
obtain ⟨a, s, rfl⟩ := f.mk'_surjective x
obtain ⟨b, t, rfl⟩ := f.mk'_surjective y
use a * t, b * s, s * t
constructor <;>
· rw [f.mk'_eq_iff_eq, Submonoid.coe_mul]
ring_nf
convert_to f.lift h (f.mk' (a + b) s) ≤ max (f.lift h _) (f.lift h _)
· refine congr_arg (f.lift h) (IsLocalization.eq_mk'_iff_mul_eq.2 ?_)
rw [add_mul, map_add]
rw [← IsLocalization.toLocalizationMap_apply S B, f.mk'_spec, f.mk'_spec,
IsLocalization.toLocalizationMap_apply, IsLocalization.toLocalizationMap_apply]
iterate 3 rw [f.lift_mk']
rw [max_mul_mul_right]
apply mul_le_mul_right' (v.map_add a b) }
