English
Let R be a commutative ring, S an R-algebra, and α ∈ S with minimal polynomial f over R. For any ideal I ⊆ R, the quotient R[α]/I is canonically isomorphic to (R/I)[x]/(f mod I), i.e. the quotient of the polynomial ring by the image of f modulo I and the quotient by I is compatible with adjoining α.
Русский
Пусть R — коммутативное кольцо, S — R-алгебра, и α ∈ S имеет минимальный многочлен f над R. Для любого идеала I ⊆ R, фактор-пространство R[α]/I изоморфно (R/I)[x]/(f mod I); совпадают структуры, соответствующая зависимость от f модуля I сохраняется.
LaTeX
$$$$ (S \\,/\\ I.map (algebraMap R S)) \\cong_R \\left( \\text{Polynomial} (R \\,/\\ I) \\;/\\ \\text{Ideal.span}\\left( \\{(\\minpoly R pb.gen).map (Ideal.Quotient.mk I)\\} \\right) \\right) $$$$
Lean4
/-- Let `α` have minimal polynomial `f` over `R` and `I` be an ideal of `R`,
then `R[α] / (I) = (R[x] / (f)) / pS = (R/p)[x] / (f mod p)`. -/
@[simps!]
noncomputable def quotientEquivQuotientMinpolyMap (pb : PowerBasis R S) (I : Ideal R) :
(S ⧸ I.map (algebraMap R S)) ≃ₐ[R]
Polynomial (R ⧸ I) ⧸ Ideal.span ({(minpoly R pb.gen).map (Ideal.Quotient.mk I)} : Set (Polynomial (R ⧸ I))) :=
(ofRingEquiv
(show
∀ x,
(Ideal.quotientEquiv _ (Ideal.map (AdjoinRoot.of (minpoly R pb.gen)) I)
(AdjoinRoot.equiv' (minpoly R pb.gen) pb (by rw [AdjoinRoot.aeval_eq, AdjoinRoot.mk_self])
(minpoly.aeval _ _)).symm.toRingEquiv
(by
rw [Ideal.map_map, AlgEquiv.toRingEquiv_eq_coe, ← AlgEquiv.coe_ringHom_commutes, ←
AdjoinRoot.algebraMap_eq, AlgHom.comp_algebraMap]))
(algebraMap R (S ⧸ I.map (algebraMap R S)) x) =
algebraMap R _ x
from fun x => by
rw [← Ideal.Quotient.mk_algebraMap, Ideal.quotientEquiv_apply, RingHom.toFun_eq_coe, Ideal.quotientMap_mk,
AlgEquiv.toRingEquiv_eq_coe, RingEquiv.coe_toRingHom, AlgEquiv.coe_ringEquiv, AlgEquiv.commutes,
Quotient.mk_algebraMap])).trans
(AdjoinRoot.quotEquivQuotMap _ _)
-- This lemma should have the simp tag but this causes a lint issue.
