English
Given x ∈ R, a localization away from x, and a map g: R → P with g(x) invertible, there exists a canonical algebra homomorphism IsLocalization.Away.lift: S → P such that it sends z = y x^{-n} to g(y) (g(x))^{-n}.
Русский
Пусть x ∈ R, существует локализация away от x, и имеется гомоморфизм g: R → P с обратимостью g(x). Тогда существует канонический алгебра-гомоморфизм IsLocalization.Away.lift: S → P с тем свойством, что z = y x^{-n} отправляется в g(y) (g(x))^{-n}.
LaTeX
$$$\\text{hg} : IsUnit(g(x)) \\Rightarrow \\text{IsLocalization.lift}: S \\to P$ с $\\text{lift}(z) = g(y) (g(x))^{-n}$ для любых $z = \\text{algebraMap}_{R,S}(y) \\cdot \\text{algebraMap}_{R,S}(x)^{-n}$$$
Lean4
/-- Given `x : R`, a localization map `F : R →+* S` away from `x`, and a map of `CommSemiring`s
`g : R →+* P` such that `g x` is invertible, the homomorphism induced from `S` to `P` sending
`z : S` to `g y * (g x)⁻ⁿ`, where `y : R, n : ℕ` are such that `z = F y * (F x)⁻ⁿ`. -/
noncomputable def lift (hg : IsUnit (g x)) : S →+* P :=
IsLocalization.lift fun y : Submonoid.powers x =>
show IsUnit (g y.1) by
obtain ⟨n, hn⟩ := y.2
rw [← hn, g.map_pow]
exact IsUnit.map (powMonoidHom n : P →* P) hg
