English
There is a lift construction: given i: R →+* S and hx, a root x with f.eval₂ i x = 0, there is a unique ring hom S → T extending i and sending the root to x.
Русский
Существует процедура подъёма: дано i: R →+* T и hx, корень x с f.eval₂ i x = 0, существует единственное кольцевое отображение S → T, расширяющее i и отправляющее корень в x.
LaTeX
$$"lift" hx : S →+* T$$
Lean4
/-- Lift a ring homomorphism `R →+* T` to `S →+* T` by specifying a root `x` of `f` in `T`,
where `S` is given by adjoining a root of `f` to `R`. -/
def lift (hx : f.eval₂ i x = 0) : S →+* T
where
toFun z := (h.repr z).eval₂ i x
map_zero' := by simp [h.eval₂_repr_eq_eval₂_of_map_eq hx _ _ (map_zero _)]
map_add' z w := by simp [h.eval₂_repr_eq_eval₂_of_map_eq hx _ (h.repr z + h.repr w)]
map_one' := by simp [h.eval₂_repr_eq_eval₂_of_map_eq hx _ _ (map_one _)]
map_mul' z w := by simp [h.eval₂_repr_eq_eval₂_of_map_eq hx _ (h.repr z * h.repr w)]
