Mestre's square decomposition

TheoremMestre's square decomposition, including the quadratic case#✓fully proved

Let \(K\) be a field of characteristic different from \(2\) and let \(d \ge 0\) be an integer. Every monic polynomial \(P \in K[X]\) of degree \(2d + 2\) can be written as \(P = Q^2 - R\) with \(Q, R \in K[X]\), \(Q\) monic of degree \(d + 1\) and \(R\) of degree at most \(d\) (possibly \(R = 0\)), and the pair \((Q, R)\) is unique.

theorem mestre_monic_square_decomposition_general
    {K : Type*} [Field K] (hchar : (2 : K) ≠ 0)
    {d : ℕ} {P : Polynomial K} (hPmonic : P.Monic) (hPdeg : P.natDegree = 2 * d + 2) :
    ∃! p : Polynomial K × Polynomial K,
      p.1.Monic ∧ p.1.natDegree = d + 1 ∧ P = p.1 ^ 2 - p.2 ∧ p.2.degree ≤ ↑d

Sources

• mestre_monic_square_decomposition is the source-shaped form, which assumes \(d \ge 1\).

Used by 1

Used byMestre's square decomposition

TheoremMestre's square decomposition#✓fully proved

Let \(K\) be a field of characteristic different from \(2\) and let \(d \ge 1\) be an integer. Every monic polynomial \(P \in K[X]\) of degree \(2d + 2\) can be written as \(P = Q^2 - R\) with \(Q, R \in K[X]\), \(Q\) monic of degree \(d + 1\) and \(R\) of degree at most \(d\) (possibly \(R = 0\)), and the pair \((Q, R)\) is unique.

theorem mestre_monic_square_decomposition
    {K : Type*} [Field K] (hchar : (2 : K) ≠ 0)
    {d : ℕ} (hd : 0 < d)
    {P : Polynomial K} (hPmonic : P.Monic) (hPdeg : P.natDegree = 2 * d + 2) :
    ∃! p : Polynomial K × Polynomial K,
      p.1.Monic ∧ p.1.natDegree = d + 1 ∧ P = p.1 ^ 2 - p.2 ∧ p.2.degree ≤ ↑d

Sources

• Arvind Suresh, "Constructing curves of high rank via composite polynomials", arXiv:2102.02113v2, https://arxiv.org/abs/2102.02113, TeX lines 1158-1179, Lemma lem:sqroot; there coefficient comparison induces a k-algebra isomorphism. Follows from mestre_monic_square_decomposition_general; the hypothesis hd is unused and keeps the source's shape.

Uses 1

Proof usesMestre's square decomposition, including the quadratic case

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.