English
For g: R → P, hg: ∀ y ∈ M, IsUnit(g(y)), and x ∈ R, y ∈ M, the equality lift hg (mk'(S, x, y)) = v holds iff g(x) = g(y) · v.
Русский
Для g: R → P, hg: ∀ y ∈ M, IsUnit(g(y)), и x ∈ R, y ∈ M, равенство lift hg (mk'(S, x, y)) = v выполняется тогда и только тогда, когда g(x) = g(y) · v.
LaTeX
$$$ lift\\;hg\\ (mk'\\ S\\ x\\ y) = v \\iff g\\ x = g\\ y \\cdot v, \\quad y \\in M. $$$
Lean4
/-- Given a localization map `f : R →+* S` for a submonoid `M ⊆ R` and a map of `CommSemiring`s
`g : R →* P` such that `g y` is invertible for all `y : M`, the homomorphism induced from
`S` to `P` maps `f x * (f y)⁻¹` to `g x * (g y)⁻¹` for all `x : R, y ∈ M`. -/
theorem lift_mk' (x y) : lift hg (mk' S x y) = g x * ↑(IsUnit.liftRight (g.toMonoidHom.restrict M) hg y)⁻¹ :=
(toLocalizationMap M S).lift_mk' _ _ _
