English
The quotient valuation on R/J has support equals to the image of supp v under the quotient map, provided J ⊆ supp v.
Русский
Опора оценивания на R/J равна образу опоры v по отображению тождества через фактор-кольцо, если J ⊆ supp v.
LaTeX
$$$\\operatorname{supp}(v^{\\mathrm{onQuot}hJ}) = (\\operatorname{supp} v).map (\\mathrm{Ideal.Quotient.mk}\, J).$$$
Lean4
/-- The quotient valuation on `R / J` has support `(supp v) / J` if `J ⊆ supp v`. -/
theorem supp_quot {J : Ideal R} (hJ : J ≤ supp v) : supp (v.onQuot hJ) = (supp v).map (Ideal.Quotient.mk J) :=
by
apply le_antisymm
· rintro ⟨x⟩ hx
apply Ideal.subset_span
exact ⟨x, hx, rfl⟩
· rw [Ideal.map_le_iff_le_comap]
intro x hx
exact hx
