English
Let R be a commutative semiring, M a submonoid of R, and S a localization of R at M. Then for x1, x2 in R and y1, y2 in M, the fractions x1/y1 and x2/y2 are equal in S if and only if the images of x1 y2 and x2 y1 in S agree, i.e. φ(x1 y2) = φ(x2 y1) where φ: R → S is the localization map.
Русский
Пусть R — коммутативная полуплексная полукольца, M — подмоном R, и S — локализация R по M. Тогда для всех x1, x2 ∈ R и y1, y2 ∈ M дроби x1/y1 и x2/y2 равны в S тогда и только тогда, когда их перекрестные произведения равны после отображения в S: φ(x1 y2) = φ(x2 y1), где φ: R → S — локализационная карта.
LaTeX
$$$\\dfrac{x_1}{y_1} = \\dfrac{x_2}{y_2} \\iff \\operatorname{algebraMap}_{R}^{S}(x_1 y_2) = \\operatorname{algebraMap}_{R}^{S}(x_2 y_1),$$$
Lean4
theorem mk'_eq_iff_eq' {x₁ x₂} {y₁ y₂ : M} :
mk' S x₁ y₁ = mk' S x₂ y₂ ↔ algebraMap R S (x₁ * y₂) = algebraMap R S (x₂ * y₁) :=
(toLocalizationMap M S).mk'_eq_iff_eq'
