English
For a power basis pb and an ideal I, applying the quotient-existence map to the image of aeval pb.gen g yields the quotient by the span of the image of the minpoly, matching g mapped under the quotient by I.
Русский
Для основанной на мощности.pb и идеала I применяемое отображение квадр.Quotient.mk к изображению aeval pb.gen g даёт эквивалентное выражение через порождение mnpoly и отображение g в фактор-пространстве, совпадающее с отображением g под Quotient.mk I.
LaTeX
$$$pb.quotientEquivQuotientMinpolyMap(I)(\\mathrm{Ideal}.Quotient.mk(I.map(\\mathrm{algebraMap} R S))(\\mathrm{aeval}_{pb.gen} g)) = \\mathrm{Ideal}.Quotient.mk(\\mathrm{Ideal}.span\\{(minpoly R pb.gen).map(\\mathrm{Ideal}.Quotient.mk I)\\} : Set (Polynomial (R / I)))(g.map(\\mathrm{Ideal}.Quotient.mk I))$$$
Lean4
theorem quotientEquivQuotientMinpolyMap_apply_mk (pb : PowerBasis R S) (I : Ideal R) (g : R[X]) :
pb.quotientEquivQuotientMinpolyMap I (Ideal.Quotient.mk (I.map (algebraMap R S)) (aeval pb.gen g)) =
Ideal.Quotient.mk (Ideal.span ({(minpoly R pb.gen).map (Ideal.Quotient.mk I)} : Set (Polynomial (R ⧸ I))))
(g.map (Ideal.Quotient.mk I)) :=
by
rw [PowerBasis.quotientEquivQuotientMinpolyMap, AlgEquiv.trans_apply, AlgEquiv.ofRingEquiv_apply, quotientEquiv_mk,
AlgEquiv.coe_ringEquiv', AdjoinRoot.equiv'_symm_apply, PowerBasis.lift_aeval, AdjoinRoot.aeval_eq,
AdjoinRoot.quotEquivQuotMap_apply_mk]
-- This lemma should have the simp tag but this causes a lint issue.
