English
There is an algebra isomorphism between the two-variable polynomial quotient and the one-variable quotient: R[X,Y] / ⟨X − Cx, Y − Cy⟩ ≅ R / ⟨x⟩.
Русский
Существует изоморфизм по алгебраическим структурам между кольцом двух переменных и одно переменной: R[X,Y] / ⟨X − Cx, Y − Cy⟩ ≅ R / ⟨x⟩.
LaTeX
$$$\\bigl( R[X,Y] / \\langle X - C x, Y - C y \\rangle \\bigr) \\cong_R R / \\langle x \\rangle$$$
Lean4
/-- For a commutative ring $R$, evaluating a polynomial at an element $y \in R$ induces an
isomorphism of $R$-algebras $R[X] / \langle x, X - y \rangle \cong R / \langle x \rangle$. -/
noncomputable def quotientSpanCXSubCAlgEquiv (x y : R) :
(R[X] ⧸ (Ideal.span {C x, X - C y} : Ideal R[X])) ≃ₐ[R] R ⧸ (Ideal.span { x } : Ideal R) :=
(Ideal.quotientEquivAlgOfEq R <| by rw [Ideal.span_insert, sup_comm]).trans <|
(DoubleQuot.quotQuotEquivQuotSupₐ R _ _).symm.trans <|
(Ideal.quotientEquivAlg _ _ (quotientSpanXSubCAlgEquiv y) rfl).trans <|
Ideal.quotientEquivAlgOfEq R <| by simp only [Ideal.map_span, Set.image_singleton]; congr 2; exact eval_C
