English
If S is an R-algebra and x ∈ S, then the natural map from R[X]/(minpoly R x) to adjoin R({x}) sends X to x and is surjective; under suitable hypotheses (R integrally closed domain and x integral) this map is an isomorphism.
Русский
Пусть S — $R$-алгебра и $x\in S$. Натуральное отображение $R[X]/(\minpoly_R(x)) \to \operatorname{adjoin}_R\{x\}$ отправляет $X$ в $x$ и является сюръекцией; при нормируемых условиях (R интегрально замкнутая область и интегральность x) это отображение изоморфизм.
LaTeX
$$$\text{toAdjoin}: \operatorname{AdjoinRoot}(\minpoly_R(x)) \to_{R} \operatorname{adjoin}_R(\{x\})$ с $X \mapsto x$; голый факт: он сюрьективен; при условии интегральной области и интегральности $x$ — изоморфизм.$$
Lean4
/-- The surjective algebra morphism `R[X]/(minpoly R x) → R[x]`.
If `R` is a integrally closed domain and `x` is integral, this is an isomorphism,
see `minpoly.equivAdjoin`. -/
def toAdjoin : AdjoinRoot (minpoly R x) →ₐ[R] adjoin R ({ x } : Set S) :=
liftHom _ ⟨x, self_mem_adjoin_singleton R x⟩ (by simp [← Subalgebra.coe_eq_zero, aeval_subalgebra_coe])
