English
Existence of a triple (z', w', d) with relations tying z and w via the map f.
Русский
Существует тройка (z', w', d), удовлетворяющая соотношениям через отображение f.
LaTeX
$$$\\exists z',w',d:\\; z f(d) = f(z') \\wedge w f(d) = f(w').$$$
Lean4
/-- Given a localization map `f : M →* N`, and `z w : N`, there exist `z' w' : M` and `d : S`
such that `f z' / f d = z` and `f w' / f d = w`. -/
@[to_additive /-- Given a localization map `f : M →+ N`, and `z w : N`, there exist `z' w' : M` and `d : S`
such that `f z' - f d = z` and `f w' - f d = w`. -/
]
theorem surj₂ (f : LocalizationMap S N) (z w : N) : ∃ z' w' : M, ∃ d : S, (z * f d = f z') ∧ (w * f d = f w') :=
by
let ⟨a, ha⟩ := surj f z
let ⟨b, hb⟩ := surj f w
refine ⟨a.1 * b.2, a.2 * b.1, a.2 * b.2, ?_, ?_⟩
· simp_rw [mul_def, map_mul, ← ha]
exact (mul_assoc z _ _).symm
· simp_rw [mul_def, map_mul, ← hb]
exact mul_left_comm w _ _
