English
Given a commutative ring A with field of fractions K, and an injective ring hom g : A →+* L where L is a field, there exists a field hom lift hg : K →+* L sending z = f x / f y to g x / g y for suitable x, y ∈ A with y non-zero-divisor.
Русский
Пусть A — коммутативное кольцо с полем дробей K, и инъективное кольцо-гомоморфизм g: A →+* L, где L — поле. Существует гомоморфизм поля hg: K →+* L, который отправляет z = f x / f y в g x / g y для подходящих x, y ∈ A, при этом y некорректно-делится.
LaTeX
$$$\text{lift}(hg) : K \to+* L$$$
Lean4
/-- Given a commutative ring `A` with field of fractions `K`,
and an injective ring hom `g : A →+* L` where `L` is a field, we get a
field hom sending `z : K` to `g x * (g y)⁻¹`, where `(x, y) : A × (NonZeroDivisors A)` are
such that `z = f x * (f y)⁻¹`. -/
noncomputable def lift (hg : Injective g) : K →+* L :=
IsLocalization.lift fun y : nonZeroDivisors A => isUnit_map_of_injective hg y
