English
Let z ∈ S and w,w' ∈ P. If z is represented by x/y in R×M, then the relation (lift z)·w + w' = v in P is equivalent to g(x)·w + g(y)·w' = g(y)·v.
Русский
Пусть z ∈ S представляется x/y в R×M. Тогда равенство (lift z)·w + w' = v в P эквивалентно g(x)·w + g(y)·w' = g(y)·v.
LaTeX
$$$ \\text{If } z \\text{ is represented by } (x,y) \\in R \\times M, \\ \\ ((\\mathrm{lift}\\,hg)\\ z) \\cdot w + w' = v \\iff g(x) \\cdot w + g(y) \\cdot w' = g(y) \\cdot v. $$$
Lean4
theorem lift_spec_mul_add {g : R →+* P} (hg : ∀ y : M, IsUnit (g y)) (z w w' v) :
((toLocalizationMap M S).lift hg) z * w + w' = v ↔
g ((toLocalizationMap M S).sec z).1 * w + g ((toLocalizationMap M S).sec z).2 * w' =
g ((toLocalizationMap M S).sec z).2 * v :=
by
rw [mul_comm, Submonoid.LocalizationMap.lift_apply, ← mul_assoc, mul_add_inv_left hg, mul_comm]
rfl
