English
Let f: S →+* R be a ring homomorphism. Then the support of the pulled-back valuation v.comap f on S equals the preimage of supp(v) under f: supp(v∘f) = Ideal.comap f (supp v).
Русский
Пусть f: S →+* R — кольцевой гомоморфизм. Тогда опора оценки, полученной на S через составление v∘f, равна обратному образу опоры v по f: supp(v∘f) = Ideal.comap f (supp v).
LaTeX
$$$\mathrm{supp}(v \circ f) = \mathrm{Ideal.comap}(f)(\mathrm{supp}(v))$$$
Lean4
theorem map_add_supp (a : R) {s : R} (h : s ∈ supp v) : v (a + s) = v a :=
by
have aux : ∀ a s, v s = 0 → v (a + s) ≤ v a := by
intro a' s' h'
refine le_trans (v.map_add a' s') (max_le le_rfl ?_)
simp [h']
apply le_antisymm (aux a s h)
calc
v a = v (a + s + -s) := by simp
_ ≤ v (a + s) := aux (a + s) (-s) (by rwa [← Ideal.neg_mem_iff] at h)
