3. Nonsingularity of algebraic curves

3.1. Powers and case splits

This section gives some extended examples “driving” polyrith. There are two basic problems requiring human workarounds that we will discuss.

The first problem arises 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. Unsurprisingly, polyrith fails.

example {x : ℚ} (hx : x ^ 2 - 4 * x = - 4) : x = 2 :=
by polyrith
-- polyrith failed to retrieve a solution from Sage! ValueError: polynomial is not in the ideal

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 :=
begin
  have : (x - 2) ^ 2 = 0 := by polyrith,
  have := pow_eq_zero this,
  polyrith,
end

The second problem arises when an argument requires the cancellation of a common factor. In the following example polyrith can deduce that \((r-1)s=(r-1) (-2)\), but the lemma mul_left_cancel₀, to cancel the common factor \(r-1\), requires a separate polyrith argument to show that it is nonzero.

example {r s : ℚ} (hr : r ≠ 1) (h : r * s - 2 = s - 2 * r) : s = -2 :=
begin
  have hr' : r - 1 ≠ 0,
  { contrapose! hr,
    polyrith },
  apply mul_left_cancel₀ hr',
  polyrith,
end

It might also happen that you can prove a factored identity with polyrith, but don’t know which of the terms is zero – or either one could be. In this case you can carry out a case split using the lemma eq_zero_or_eq_zero_of_mul_eq_zero or similar.

example {r s : ℚ} (h : r * s - 2 = s - 2 * r) : true :=
begin
  have : (r - 1) * (s + 2) = 0 := by polyrith,
  cases eq_zero_or_eq_zero_of_mul_eq_zero this with H H,
  { sorry }, -- the case `r - 1 = 0`
  { sorry } -- the case `s + 2 = 0`
end

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

\[\begin{split}\begin{pmatrix} \partial_xp(x,y,z)\\ \partial_yp(x,y,z)\\ \partial_zp(x,y,z) \end{pmatrix}\end{split}\]

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\).

@[reducible] def klein : mv_polynomial (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

\[\begin{split}\begin{pmatrix} 3x^2y + z ^ 3\\ x ^ 3 + 3y^2z\\ y ^ 3 + 3z ^ 2x \end{pmatrix}.\end{split}\]

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\).

Here is a possible approach: By eye, looking at appropriate multiples

\[x(3x^2y + z ^ 3), \qquad y(x ^ 3 + 3y^2z), \qquad z(y ^ 3 + 3z ^ 2x)\]

of the vector of partial derivatives, I can see that we have three different linear combinations of \(x^3y\), \(y^3z\) and \(z^3x\) which vanish. So use polyrith to prove that, say, \(y^3z=0\).

Now do a case split, deducing that either \(y^3 = 0\) or \(z = 0\). Deduce using pow_eq_zero that in the former case \(y = 0\).

In either case, polyrith now has enough information to deduce that the cubes of the remaining variables vanish. Apply pow_eq_zero again to deduce that the variables themselves vanish.

Once you have hypotheses hx, hy, hz for the vanishing of the three variables, you can solve the problem with simp [hx, hy, hz].

example {x y z : K} (h : mv_polynomial.eval ![x, y, z] (klein K) = 0)
  (hdz : ∀ i, mv_polynomial.eval ![x, y, z] (mv_polynomial.pderiv i (klein K)) = 0) :
  ![x, y, z] = 0 :=
begin
  have : 3 - 1 = 2 := by norm_num,
  have h₀ := hdz 0,
  have h₁ := hdz 1,
  have h₂ := hdz 2,
  simp only [this] with poly_simps at h h₀ h₁ h₂ {discharger := `[norm_num1]},
  sorry,
end

3.3. Weierstrass-form elliptic curve

Next, we consider an elliptic curve in Weierstrass normal form \(zy^2 = x^3 + pxz^2 + qz^3\).

a Weierstrass-normal-form elliptic curve — Fig. 3.2 A Weierstrass-normal-form elliptic curve with positive discriminant.

We fix the parameters \(p\) and \(q\) explicitly.

variables (p q : K)

@[reducible] def weierstrass : mv_polynomial (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

\[\begin{split}\begin{pmatrix} 3x ^ 2 + pz ^ 2\\ -2yz\\ -y ^ 2 + 2pxz + 3qz ^ 2 \end{pmatrix}.\end{split}\]

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, then \(27q^2+4p^3\) vanishes.

A possible approach is as follows. First do a case split depending on whether we are on the line at infinity, \(z=0\). If we are on the line at infinity, polyrith will give you the vanishing of certain powers of \(x\) and \(y\) (you’ll need to work out which). Apply pow_eq_zero as needed. Once you have hypotheses hx, hy, hz for the vanishing of the three variables, you can solve the problem with simp [hx, hy, hz].

Away from the line at infinity, we have that \(z\ne 0\). If the polynomial and its partial derivatives vanish at such an \([x:y:z]\), we successively deduce that \(y=0\), that \(2 p x + 3 q z = 0\), that \(9 q x - 2 p ^ 2 z=0\), and that \(27q^2+4p^3=0\). For each of these four polyrith deductions you will have to apply mul_left_cancel₀ with the nonvanishing of \(z\): each time the expression itself is not in the ideal but its product with \(z\) is.

example {x y z : K} (disc : 27 * q ^ 2 + 4 * p ^ 3 ≠ 0)
  (h : mv_polynomial.eval ![x, y, z] (weierstrass K p q) = 0)
  (hdz : ∀ i, mv_polynomial.eval ![x, y, z] (mv_polynomial.pderiv i (weierstrass K p q)) = 0) :
  ![x, y, z] = 0 :=
begin
  have three_sub : 3 - 1 = 2 := by norm_num,
  have two_sub : 2 - 1 = 1 := by norm_num,
  have h₀ := hdz 0,
  have h₁ := hdz 1,
  have h₂ := hdz 2,
  simp only [three_sub, two_sub] with poly_simps at h h₀ h₁ h₂ {discharger := `[norm_num1]},
  sorry,
end