English
Given F-algebras S, T and an element x ∈ S, y ∈ T with h: aeval y(minpoly F x) = 0, there exists a unique F-algebra hom from Adjoin F {x} to T sending x to y; this is obtained by composing the canonical equivalence with AdjoinRoot.liftHom.
Русский
Пусть есть F-алгебры S, T, элемент x ∈ S и y ∈ T с условием h: aeval y(minpoly F x) = 0. Тогда существует единственный F-алгебра-гомоморфизм от Adjoin F {x} в T, отправляющий x в y; он получается как композиция с AdjoinRoot.liftHom.
LaTeX
$$$\\exists !\\, \\varphi: \\mathrm{adjoin}_F\\{x\\} \\to_F T\\text{ с }\\varphi(x)=y \\text{, если } aeval_y(minpoly F x)=0$$$
Lean4
/-- Produce an algebra homomorphism `Adjoin R {x} →ₐ[R] T` sending `x` to
a root of `x`'s minimal polynomial in `T`. -/
noncomputable def liftSingleton {S T : Type*} [CommRing S] [CommRing T] [Algebra F S] [Algebra F T] (x : S) (y : T)
(h : aeval y (minpoly F x) = 0) : Algebra.adjoin F { x } →ₐ[F] T :=
(AdjoinRoot.liftHom _ y h).comp (AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly F x).toAlgHom
