English
There is a canonical isomorphism between AdjoinRoot f modulo I and (R/I)[X] modulo (f mod I) expressed via a chain of quotient-polynomial equivalences.
Русский
Существует канонический изоморфизм между AdjoinRoot f/ I и (R/I)[X]/(f mod I), выраженный через последовательность эквивалентностей по многочленам и квотам.
LaTeX
$$$\text{quotAdjoinRootEquivQuotPolynomialQuot}: AdjoinRoot f ⧸ I.map(\mathrm{of} f) \cong+* (R \otimes I) [X] / \langle f\rangle$ (последовательность эквививалентностей).$$
Lean4
/-- The natural isomorphism `(R/I)[x]/(f mod I) ≅ (R[x]/I*R[x])/(f mod I[x])` where
`f : R[X]` and `I : Ideal R` -/
def quotQuotEquivComm :
(R ⧸ I)[X] ⧸ span ({f.map (Ideal.Quotient.mk I)} : Set (Polynomial (R ⧸ I))) ≃+*
(R[X] ⧸ (I.map C)) ⧸ span ({(Ideal.Quotient.mk (I.map C)) f} : Set (R[X] ⧸ (I.map C))) :=
quotientEquiv (span ({f.map (Ideal.Quotient.mk I)} : Set (Polynomial (R ⧸ I))))
(span {Ideal.Quotient.mk (I.map Polynomial.C) f}) (polynomialQuotientEquivQuotientPolynomial I)
(by
rw [map_span, Set.image_singleton, RingEquiv.coe_toRingHom, polynomialQuotientEquivQuotientPolynomial_map_mk I f])
