English
There is a canonical way to lift an injective polynomial-ring homomorphism φ: R[X] → L to a RatFunc-R →+* L, by sending a fraction n/d to φ(n)/φ(d). This extension is well-defined on nonzero-divisors and preserves ring operations.
Русский
Существует каноническое продолжение инъективного гомоморфизма φ: R[X] → L до гомоморфизма RatFunc R →+* L, отправляющего дробь n/d в φ(n)/φ(d). Расширение определено на ненулевым делителям и сохраняет операции умножения и сложения.
LaTeX
$$$\\exists \\psi: RatFunc R \\to+* L \\text{ с } \\psi(n/d)=\\phi(n)/\\phi(d) \\text{ и } \\psi \\text{ сохраняет структуру кольца (рациональные функции).}$$$
Lean4
/-- Lift an injective ring homomorphism `R[X] →+* L` to a `RatFunc R →+* L`
by mapping both the numerator and denominator and quotienting them. -/
def liftRingHom (φ : R[X] →+* L) (hφ : R[X]⁰ ≤ L⁰.comap φ) : RatFunc R →+* L :=
{ liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ with
map_add' := fun x y => by
simp only [ZeroHom.toFun_eq_coe, MonoidWithZeroHom.toZeroHom_coe]
cases subsingleton_or_nontrivial R
· rw [Subsingleton.elim (x + y) y, Subsingleton.elim x 0, map_zero, zero_add]
obtain ⟨x⟩ := x
obtain ⟨y⟩ := y
cases x using Localization.induction_on with
| _ pq
cases y using Localization.induction_on with
| _ p'q'
obtain ⟨p, q⟩ := pq
obtain ⟨p', q'⟩ := p'q'
rw [← ofFractionRing_add, Localization.add_mk]
simp only [RingHom.toMonoidWithZeroHom_eq_coe, liftMonoidWithZeroHom_apply_ofFractionRing_mk]
rw [div_add_div, div_eq_div_iff]
· rw [mul_comm _ p, mul_comm _ p', mul_comm _ (φ p'), add_comm]
simp only [map_add, map_mul, Submonoid.coe_mul]
all_goals
try simp only [← map_mul, ← Submonoid.coe_mul]
exact nonZeroDivisors.ne_zero (hφ (SetLike.coe_mem _)) }
