English
For a fixed ring R and W' affine over R, the XY-ideal with polynomial constant C y equals the XY-ideal with linePolynomial x y ℓ for any x, y, ℓ with W' equations, reflecting a linear equivalence along the line.
Русский
Для заданного кольца R и W' аффинной кривой над R, XY-идеал с C y равен XY-идеалу с linePolynomial x y ℓ при любых x, y, ℓ, удовлетворяющих уравнениям W'.
LaTeX
$$$XYIdeal W'\' x (C y) = XYIdeal W' x (linePolynomial x y \ell)$$$
Lean4
theorem XYIdeal_add_eq (x₁ x₂ y₁ ℓ : R) :
XYIdeal W' (W'.addX x₁ x₂ ℓ) (C <| W'.addY x₁ x₂ y₁ ℓ) =
.span {mk W' <| W'.negPolynomial - C (linePolynomial x₁ y₁ ℓ)} ⊔ XIdeal W' (W'.addX x₁ x₂ ℓ) :=
by
simp only [XYIdeal, XIdeal, XClass, YClass, addY, negAddY, negY, negPolynomial, linePolynomial]
rw [sub_sub <| -(Y : R[X][Y]), neg_sub_left (Y : R[X][Y]), map_neg, span_singleton_neg, sup_comm, ← span_insert, ←
span_pair_add_mul_right <| mk W' <| C <| C <| W'.a₁ + ℓ, ← map_mul, ← map_add]
apply congr_arg (_ ∘ _ ∘ _ ∘ _)
C_simp
ring1
