liftRingHom_apply_ofFractionRing_mk

English

Given φ: R[X] →+* L, hφ and p, q, one has a lifted map that preserves divisibility and multiplication across RatFunc.

Русский

Дано φ: R[X] →+* L и условие hφ. Существуют свойства вытяжки, сохраняющие делимость и умножение при переходе к RatFunc.

LaTeX

$$$\\text{Lift preserves } \\frac{p}{q} \\mapsto \\frac{\\phi(p)}{\\phi(q)}$ under nonzero-divisors.$$

Lean4

theorem liftRingHom_apply_ofFractionRing_mk (φ : R[X] →+* L) (hφ : R[X]⁰ ≤ L⁰.comap φ) (n : R[X]) (d : R[X]⁰) :
    liftRingHom φ hφ (ofFractionRing (Localization.mk n d)) = φ n / φ d :=
  liftMonoidWithZeroHom_apply_ofFractionRing_mk _ hφ _ _

Похожие утверждения