English
Let W be a Weierstrass affine curve over a field F. For any nonsingular pair (x, y) in F, the fractional ideal of the function field F(W) generated by X − x and Y − y is a unit (i.e., invertible) in the fractional ideal group associated to W.
Русский
Пусть W — аффинная кривая Вейерштрасса над полем F. Для любого невырожденного пара (x, y) из F дробный идеал функции поля F(W), порожденный X − x и Y − y, является единичным элементом (обратимым) в группе дробных идеалов, связанной с W.
LaTeX
$$$XYIdeal'(h) \\in \\left( \\operatorname{FractionalIdeal}\\left(W.CoordinateRing^0 W.FunctionField\\right) \\right)^{\\times}$$$
Lean4
/-- The non-zero fractional ideal `⟨X - x, Y - y⟩` of `F(W)` for some `x` and `y` in `F`. -/
noncomputable def XYIdeal' {x y : F} (h : W.Nonsingular x y) : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ :=
Units.mkOfMulEqOne _ _ <| by
rw [← mul_assoc, ← coeIdeal_mul, mul_comm <| XYIdeal W .., XYIdeal_neg_mul h, XIdeal,
FractionalIdeal.coe_ideal_span_singleton_mul_inv W.FunctionField <| XClass_ne_zero x]
