English
Let φ: K[X] → L be a ring hom into a field L, and let hφ be a compatibility condition on non-zero divisors. Then the lift of φ to RatFunc satisfies the natural compatibility with division: liftRingHom φ hφ (algebraMap K[X] p / algebraMap K[X] q) = φ(p) / φ(q) for p, q ∈ K[X], with q ≠ 0.
Русский
Пусть φ: K[X] → L — гомоморф кольца в поле L, пусть hφ — условие совместимости для нуль-делителей. Тогда тяг (lifting) φ к RatFunc удовлетворяет естественной совместимости с делением: liftRingHom φ hφ(алгебраобразная доля p / q) = φ(p) / φ(q) для p, q ∈ K[X] и q ≠ 0.
LaTeX
$$$ \operatorname{liftRingHom}(\varphi, h_\varphi)\left(\dfrac{p}{q}\right) = \dfrac{\varphi(p)}{\varphi(q)} \quad(p,q \in K[X], q \neq 0)$$$
Lean4
theorem liftRingHom_apply_div {L : Type*} [Field L] (φ : K[X] →+* L) (hφ : K[X]⁰ ≤ L⁰.comap φ) (p q : K[X]) :
liftRingHom φ hφ (algebraMap _ _ p / algebraMap _ _ q) = φ p / φ q :=
liftMonoidWithZeroHom_apply_div _ hφ _ _
