Valuative comparisons in a localization

Clear denominators in a valuative relation on a localization of a commutative semiring. The localized denominators are units, so multiplication by them preserves comparisons and nonvanishing. These facts also describe pullback on valuation spectra of rings.

theorem ValuativeRel.vle_mk'_iff {A : Type u_1} [CommSemiring A] (S : Submonoid A) (B : Type u_2) [CommSemiring B] [Algebra A B] [IsLocalization S B] [ValuativeRel B] (a₁ a₂ : A) (s₁ s₂ : ↥S) : IsLocalization.mk' B a₁ s₁ ≤ᵥ IsLocalization.mk' B a₂ s₂ ↔ (algebraMap A B) (a₁ * ↑s₂) ≤ᵥ (algebraMap A B) (a₂ * ↑s₁)

A comparison between two localization fractions is equivalent to the comparison obtained by clearing their denominators.

theorem ValuativeRel.not_vle_algebraMap_mul_den_zero_iff {A : Type u_1} [CommSemiring A] (S : Submonoid A) (B : Type u_2) [CommSemiring B] [Algebra A B] [IsLocalization S B] [ValuativeRel B] (a : A) (s t : ↥S) : ¬(algebraMap A B) (a * ↑s) ≤ᵥ 0 ↔ ¬IsLocalization.mk' B a t ≤ᵥ 0

Multiplying a numerator by a localized denominator or placing it over any denominator does not change whether its value is nonzero.