English
Given a gcd-domain, a localization M → A yields elements a,b in the base ring whose gcd is a unit and such that z is represented by a fraction with denominator b in the localization.
Русский
Для gcd-доменa локализация M → A дает элементы a,b базовой кольца, чьи НОД является единицей, и такое, что z представимо как a/ b в локализации.
LaTeX
$$$\\exists a,b \\in R$, IsUnit$(\\gcd\\ a\\ b)$ ∧ z \\cdot algebraMap\\ R\\, A\\, b = algebraMap\\ R\\, A\\, a$$$
Lean4
theorem surj_of_gcd_domain [GCDMonoid R] (M : Submonoid R) [IsLocalization M A] (z : A) :
∃ a b : R, IsUnit (gcd a b) ∧ z * algebraMap R A b = algebraMap R A a :=
by
obtain ⟨x, ⟨y, hy⟩, rfl⟩ := IsLocalization.mk'_surjective M z
obtain ⟨x', y', hx', hy', hu⟩ := extract_gcd x y
use x', y', hu
rw [mul_comm, IsLocalization.mul_mk'_eq_mk'_of_mul]
convert IsLocalization.mk'_mul_cancel_left (M := M) (S := A) _ _ using 2
grind
