English
LiftHom is the canonical algebra map from IsAdjoinRoot S f to T, lifting the R-algebra structure and the chosen root. It is equal to h.lift (algebraMap R T) x hx'.
Русский
LiftHom — каноническое отображение из IsAdjoinRoot S f в T, поднимающее R-алгебраическую структуру и выбранный корень. Оно равняется h.lift (algebraMap R T) x hx'.
LaTeX
$$$ h.liftHom x hx' : S \to_{\!R} T = h.lift (algebraMap R T) x hx' $$$
Lean4
/-- Lift the algebra map `R → T` to `S →ₐ[R] T` by specifying a root `x` of `f` in `T`,
where `S` is given by adjoining a root of `f` to `R`. -/
def liftHom : S →ₐ[R] T :=
{ h.lift (algebraMap R T) x hx' with commutes' a := h.lift_algebraMap hx' a }
