English
There is a lift of an injective polynomial algebra map to a RatFunc-algebra map, i.e., RatFunc K → RatFunc L with the desired properties.
Русский
Существует подъем инъективного алгебра-гомоморфа K[X] → L к алгебра-гомоморфе RatFunc K → RatFunc L.
LaTeX
$$$\text{liftAlgHom} : RatFunc K \to RatFunc L$ with properties extending the polynomial map$$
Lean4
/-- Lift an injective algebra homomorphism `K[X] →ₐ[S] L` to a `RatFunc K →ₐ[S] L`
by mapping both the numerator and denominator and quotienting them. -/
def liftAlgHom : RatFunc K →ₐ[S] L :=
{ liftRingHom φ.toRingHom hφ with
commutes' := fun r => by
simp_rw [RingHom.toFun_eq_coe, AlgHom.toRingHom_eq_coe, algebraMap_apply r, liftRingHom_apply_div,
AlgHom.coe_toRingHom, map_one, div_one, AlgHom.commutes] }
