English
The symmetric version of the previous quotient map'sMk-applied form holds: the symmetrized application of the quotient isomorphism to a mk of the span by minpoly yields the same quotient as above with g mapped accordingly.
Русский
Симметричная версия отображения через квотирование сохраняется: применение симметричного отображения изоморфизма к mk остаётся тем же результатом, что и выше с соответствующим отображением g.
LaTeX
$$$$ (pb.quotientEquivQuotientMinpolyMap I).symm (\operatorname{Ideal.Quotient.mk} (\operatorname{Ideal.span}({(minpoly R pb.gen).map (Ideal.Quotient.mk I)} : Set (Polynomial (R ⧸ I)))) (g.map (Ideal.Quotient.mk I))) = \operatorname{Ideal.Quotient.mk} (I.map (algebraMap R S)) (\operatorname{aeval pb.gen} g) $$$$
Lean4
theorem quotientEquivQuotientMinpolyMap_symm_apply_mk (pb : PowerBasis R S) (I : Ideal R) (g : R[X]) :
(pb.quotientEquivQuotientMinpolyMap I).symm
(Ideal.Quotient.mk (Ideal.span ({(minpoly R pb.gen).map (Ideal.Quotient.mk I)} : Set (Polynomial (R ⧸ I))))
(g.map (Ideal.Quotient.mk I))) =
Ideal.Quotient.mk (I.map (algebraMap R S)) (aeval pb.gen g) :=
by
simp only [quotientEquivQuotientMinpolyMap, toRingEquiv_eq_coe, symm_trans_apply, quotEquivQuotMap_symm_apply_mk,
ofRingEquiv_symm_apply, quotientEquiv_symm_mk, RingEquiv.symm_symm, AdjoinRoot.equiv'_apply, coe_ringEquiv,
liftHom_mk, symm_toRingEquiv]
