English
There is a canonical algebra homomorphism that lifts an algebra map on polynomials to a map RatFunc K → RatFunc R, provided the map sends non-zero-divisors to non-zero-divisors.
Русский
Существует канонический алгебра-гомоморф, поднимающий тождественную алгебра-гомоморфию K[X] → S R[X] до расщепляющего гомоморфа RatFunc K → RatFunc R, если образ отправляет нуль-делители в нуль-делители.
LaTeX
$$$\text{mapAlgHom}(\varphi, h_\varphi) : RatFunc K \to RatFunc R$$$
Lean4
/-- Lift an algebra homomorphism that maps polynomials `φ : K[X] →ₐ[S] R[X]`
to a `RatFunc K →ₐ[S] RatFunc R`,
on the condition that `φ` maps non-zero-divisors to non-zero-divisors,
by mapping both the numerator and denominator and quotienting them. -/
def mapAlgHom (φ : K[X] →ₐ[S] R[X]) (hφ : K[X]⁰ ≤ R[X]⁰.comap φ) : RatFunc K →ₐ[S] RatFunc R :=
{ mapRingHom φ hφ with
commutes' := fun r => by
simp_rw [RingHom.toFun_eq_coe, coe_mapRingHom_eq_coe_map, algebraMap_apply r, map_apply_div, map_one,
AlgHom.commutes] }
