English
There exists a ring isomorphism between S/I.map(algebraMap R S) and (R/I)[X] modulo the span of the image of minpoly.
Русский
Существуют изоморфизмы колец между S/(I.map) и (R/I)[X] / ⟨minpoly⟩.
LaTeX
$$$$ S / I.map(\,\,\text{algebraMap } R S) \cong (R / I)[X] / \langle (\minpoly R x)^{\sim} \rangle. $$$$
Lean4
theorem quotMapEquivQuotQuotMap_symm_apply (hx : (conductor R x).comap (algebraMap R S) ⊔ I = ⊤) (hx' : IsIntegral R x)
(Q : R[X]) : (quotMapEquivQuotQuotMap hx hx').symm (Q.map (Ideal.Quotient.mk I)) = Q.aeval x :=
by
apply (quotMapEquivQuotQuotMap hx hx').injective
rw [quotMapEquivQuotQuotMap, AlgEquiv.toRingEquiv_eq_coe, RingEquiv.symm_trans_apply, RingEquiv.symm_symm,
RingEquiv.coe_trans, Function.comp_apply, RingEquiv.symm_apply_apply, RingEquiv.symm_trans_apply,
quotEquivOfEq_symm, quotEquivOfEq_mk]
congr
convert (adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap_symm_apply_mk I Q
apply (quotAdjoinEquivQuotMap hx (FaithfulSMul.algebraMap_injective ((adjoin R { x })) S)).injective
simp only [RingEquiv.apply_symm_apply, adjoin.powerBasis'_gen, quotAdjoinEquivQuotMap_apply_mk, coe_aeval_mk_apply]
