3. Nonsingularity of algebraic curves
3.1. Powers and cancellation
In this section we study some problems from algebraic geometry:
proving the nonsingularity of certain algebraic curves.
These are good case studies for working with polyrith
in which one needs slightly more than the basic Gröbner basis algorithm.
Before starting on the case studies,
let me demonstrate the two techniques I will use in them to get a bit more out of polyrith,
one built-in and one requiring a human work-around.
The first technique is relevant when the ideal generated by the hypothesis polynomials is not radical. In the following example, \(x-2\) (the goal polynomial) does not belong to the ideal generated by \(x ^ 2 - 4 x + 4=(x-2)^2\), but only to its radical.
This can be worked around by applying a lemma such as pow_eq_zero, which states that if a power
of an expression is zero then the expression is also zero.
example {x : ℤ} (hx : x ^ 2 - 4 * x = -4) : x = 2 := by
have H : (x - 2) ^ 2 = 0 := by linear_combination hx
apply pow_eq_zero at H
linear_combination H
This is a sufficiently common pattern that linear_combination provides a shorthand syntax,
allowing you to specify the power of the goal polynomial
which lies in the ideal generated by the hypothesis polynomials.
-- hover over the `(exp := 2)` to get a useful explanation in a pop-up
example {x : ℚ} (hx : x ^ 2 - 4 * x = - 4) : x = 2 := by linear_combination (exp := 2) hx
And in fact polyrith can find certificates of this form too –
there’s a “standard trick” for testing membership in the radical
without doing a naive search for the exponent.
Check out Section 2.2 of this article of Pottier,
or Section 4.2 of Cox, Little, O’Shea’s Ideals, Varieties, and Algorithms.
example {x : ℚ} (hx : x ^ 2 - 4 * x = - 4) : x = 2 := by polyrith
-- produces `linear_combination (exp := 2) hx`
Here are a few more examples which polyrith can solve in this way.
Click through to see the certificates produced.
example {a b : ℝ} (h₁ : a ^ 2 = 2 * b ^ 2) (h₂ : b ^ 2 = 2 * a ^ 2) : a = 0 := by
polyrith
example {x y z : ℚ} (h₁ : x = y) (h₂ : x * y = 0) : x + y * z = 0 := by
polyrith
The second technique applies when,
as is often the case in an algebraic problem,
you have some information about disequalities
(hypotheses \(A\ne B\)) as well as equalities.
A convenient way to exploit such information when working with polyrith
is to multiply the goal through by the quantity that is thus known to be nonzero.
(That’s the backwards-reasoning description;
the forwards-reasoning description is
“prove a carefully constructed intermediate fact and then cancel the common nonzero factor”.)
For example, consider the following problem.
Problem
Let \(z\) be a complex number such that \(z^3=1\) and \(z\ne 1\). Show that
To solve this problem, we note that since \(z-1\ne 0\),
it will suffice to prove that \((z-1)(z^2+z+1)\ne (z-1)\cdot 0\).
(The lemma mul_left_cancel₀ can perform this reduction.)
The new goal is a linear_combination of the hypothesis \(z^3=1\).
example {z : ℂ} (h₁ : z ^ 3 = 1) (h₂ : z ≠ 1) : z ^ 2 + z + 1 = 0 := by
rw [← sub_ne_zero] at h₂
apply mul_left_cancel₀ h₂
polyrith
Here are a couple of exercises along these lines.
example {a b c d e f : ℤ} (h₁ : a * d = b * c) (h₂ : c * f = d * e) (hd : d ≠ 0) :
a * f = b * e := by
sorry
example {r s : ℚ} (hr : r ≠ 1) (h : r * s - 2 = s - 2 * r) : s = -2 := by
sorry
3.2. Klein quartic
Fix a field \(K\) of characteristic zero. A homogenous polynomial in three variables \(p(x,y,z)\) defines an algebraic curve \(\{[x:y:z]\in K\mathbb{P}^2:p(x,y,z)=0\}\) in the projective plane \(K\mathbb{P}^2\).
This curve is said to be nonsingular, if there is no point on the curve where the vector of partial derivatives
vanishes entirely.
In this section and the next we prove the nonsingularity of a couple of examples of curves in the projective plane.
First we consider the Klein quartic curve \(x^3y + y^3z + z^3x = 0\).
Fig. 3.1 The Klein quartic restricted to the real affine plane \(x+y+z= 1\).
/-- Defining polynomial for the Klein quartic curve x³y + y³z + z³x = 0 as a projective
hypersurface in Kℙ². -/
abbrev klein : MvPolynomial (Fin 3) K :=
X 0 ^ 3 * X 1 + X 1 ^ 3 * X 2 + X 2 ^ 3 * X 0
The vector of partial derivatives of this polynomial is
We need to show that there is nowhere on the curve where these three cubic polynomials all vanish, or equivalently that if these three polynomials and the quartic \(x^3y + y^3z + z^3x\) all vanish then \(x=y=z=0\).
polyrith can do this:
it will find that \(x^6\), \(y^6\) and \(z^6\) are all in the ideal generated by these four polynomials.
Try it!
/-- The Klein quartic is nonsingular. -/
example {x y z : K} (h : MvPolynomial.eval ![x, y, z] (klein K) = 0)
(hdz : ∀ i, MvPolynomial.eval ![x, y, z] (MvPolynomial.pderiv i (klein K)) = 0) :
![x, y, z] = 0 := by
have h₀ := hdz 0
have h₁ := hdz 1
have h₂ := hdz 2
simp [map_ofNat] at h h₀ h₁ h₂
ext i
fin_cases i <;> dsimp
· polyrith
· polyrith
· polyrith
3.3. Weierstrass-form elliptic curve
Next, we consider an elliptic curve in Weierstrass normal form \(zy^2 = x^3 + pxz^2 + qz^3\).
Fig. 3.2 A Weierstrass-normal-form elliptic curve with positive discriminant.
We fix the parameters \(p\) and \(q\) explicitly.
variable (p q : K)
/-- Defining polynomial for a Weierstrass-form elliptic curve zy² = x³ + pxz² + qz³ as a
projective hypersurface in Kℙ². -/
abbrev weierstrass : MvPolynomial (Fin 3) K :=
-X 2 * X 1 ^ 2 + X 0 ^ 3 + C p * X 0 * X 2 ^ 2 + C q * X 2 ^ 3
The vector of partial derivatives of this polynomial is
It turns out that a Weierstrass-form elliptic curve is nonsingular if its discriminant, \(27q^2+4p^3\), does not vanish. To prove this we need to show that if there is a (nonzero) point \([x:y:z]\) where the polynomial and its partial derivatives vanish and \(27q^2+4p^3\) does not, then \(x=y=z=0\).
To make use of a nonzeroness condition,
it is useful to multiply the goal through by the nonzero quantity:
in this case the goal \((27q^2+4p^3)x=(27q^2+4p^3) \cdot 0\) is accessible to polyrith although \(x=0\) is not.
The lemma mul_left_cancel₀ will be helpful here.
polyrith should show you that \(\left((27q^2+4p^3)x\right)^4\),
\(\left((27q^2+4p^3)y\right)^3\) and \(\left((27q^2+4p^3)z\right)^5\)
are all in the ideal generated by the four hypothesis polynomials.
The coefficients are pretty wild – I saw numbers like 944,784 and 2,204,496.
If you like, you can get shorter polyrith certificates at the cost of more setup.
The polynomials \((27q^2+4p^3)x^4\), \((27q^2+4p^3)y^3\) and \((27q^2+4p^3)z^5\) are all in the ideal as well,
and you can reduce the problem to these three goals by some initial work with the lemmas pow_eq_zero and mul_left_cancel₀.
/-- A Weierstrass-form elliptic curve with nonzero discriminant `27 * q ^ 2 + 4 * p ^ 3` is
nonsingular. -/
example {x y z : K} (disc : 27 * q ^ 2 + 4 * p ^ 3 ≠ 0)
(h : MvPolynomial.eval ![x, y, z] (weierstrass K p q) = 0)
(hdz : ∀ i, MvPolynomial.eval ![x, y, z] (MvPolynomial.pderiv i (weierstrass K p q)) = 0) :
![x, y, z] = 0 := by
have h₀ := hdz 0
have h₁ := hdz 1
have h₂ := hdz 2
simp [map_ofNat] at h h₀ h₁ h₂
ext i
fin_cases i <;> dsimp
· sorry
· sorry
· sorry