English
For a commutative ring R and W' affine over R, the XY-ideal of the sum coordinates with respect to the line equals the supremum of the principal span generated by the negative line polynomial and the X-ideal of the sum.
Русский
Для коммутативного кольца R и W' аффинной кривой над R, XY-идеал суммы по координатам и линии равен наибольшему элементу над идеалом порождённым линейным полиномом и X-идеалом суммы.
LaTeX
$$$XYIdeal W' (W'.addX x_1 x_2 \ell) (C(W'.addY x_1 x_2 y_1 \ell)) = \mathrm{span}\{mk W'(W'.negPolynomial - C(linePolynomial x_1 y_1 \ell))\} \;\sqcup\; XIdeal W'(W'.addX x_1 x_2 \ell)$$$
Lean4
/-- The `R`-algebra isomorphism from `R[W] / ⟨X - x, Y - y(X)⟩` to `R` obtained by evaluation at
some `y(X)` in `R[X]` and at some `x` in `R` provided that `W(x, y(x)) = 0`. -/
noncomputable def quotientXYIdealEquiv {x : R} {y : R[X]} (h : (W'.polynomial.eval y).eval x = 0) :
(W'.CoordinateRing ⧸ XYIdeal W' x y) ≃ₐ[R] R :=
((quotientEquivAlgOfEq R <| by simp only [XYIdeal, XClass, YClass, ← Set.image_pair, ← map_span]; rfl).trans <|
DoubleQuot.quotQuotEquivQuotOfLEₐ R <|
(span_singleton_le_iff_mem _).mpr <| mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero.mpr h).trans
quotientSpanCXSubCXSubCAlgEquiv
