Division polynomials in characteristic p are p-th power substitutions

In characteristic p the low division polynomials of a Weierstrass curve lie in the image of Polynomial.expand R p, that is, they are polynomials in Xᵖ. This is the base case of the factorisation of the p-power isogeny through Frobenius (Silverman III.6.2): the terms that obstruct it all carry a factor of p.

Concretely, in characteristic 2 the 2 * b₆ * X term of Φ₂ and the 4X³, 2b₄X terms of ΨSq₂ vanish; in characteristic 3 the 3X⁴, 3b₄X², 3b₆X terms of Ψ₃ vanish. Everything is stated over an arbitrary commutative ring carrying CharP, so it specialises unchanged to a field or to a universal polynomial ring.

Main results

• WeierstrassCurve.Φ_two_mem_range_expand, ΨSq_two_mem_range_expand: characteristic two.
• WeierstrassCurve.Ψ₃_mem_range_expand, ΨSq_three_mem_range_expand, Φ_three_mem_range_expand: characteristic three.

Provenance

Ported from the AINTLIB HasseWeil project (Apache-2.0), revision 513e83879e2f, file HasseWeil/Verschiebung/DivPolyExpand.lean, declarations Φ_two_mem_expand_two_charP, ΨSq_two_mem_expand_two_charP, Ψ₃_mem_expand_three_charP, ΨSq_three_mem_expand_three_charP and Φ_three_mem_expand_three_charP.

The source's b_relation_of_charP_three is not ported: Mathlib already has it verbatim as WeierstrassCurve.b_relation_of_char_three (Weierstrass.lean:213).

The source's proof of Φ_three_mem_expand_three_charP raises the elaboration heartbeat limit to five times the default, which this repository forbids. The witness cubic and the linear_combination strategy here are the source's (its multipliers are symbolically verified over ℤ, as there); substituting the characteristic-three b-relation at the C-level inside the linear_combination, rather than rewriting it into the goal, is what lets the same argument elaborate within the default budget.

theorem WeierstrassCurve.Φ_two_mem_range_expand {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [CharP R 2] : W.Φ 2 ∈ Set.range ⇑(Polynomial.expand R 2)

In characteristic two, Φ₂ is a polynomial in X².

Φ₂ = X⁴ − b₄X² − 2b₆X − b₈, and the 2b₆X term vanishes.

theorem WeierstrassCurve.ΨSq_two_mem_range_expand {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [CharP R 2] : W.ΨSq 2 ∈ Set.range ⇑(Polynomial.expand R 2)

In characteristic two, ΨSq₂ is a polynomial in X².

ΨSq₂ = Ψ₂Sq = 4X³ + b₂X² + 2b₄X + b₆, and the 4X³ and 2b₄X terms vanish.

theorem WeierstrassCurve.Ψ₃_mem_range_expand {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [CharP R 3] : W.Ψ₃ ∈ Set.range ⇑(Polynomial.expand R 3)

In characteristic three, Ψ₃ is a polynomial in X³.

Ψ₃ = 3X⁴ + b₂X³ + 3b₄X² + 3b₆X + b₈, and every term with a factor of 3 vanishes.

theorem WeierstrassCurve.ΨSq_three_mem_range_expand {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [CharP R 3] : W.ΨSq 3 ∈ Set.range ⇑(Polynomial.expand R 3)

In characteristic three, ΨSq₃ is a polynomial in X³, since it is Ψ₃² and expand is multiplicative.

theorem WeierstrassCurve.Φ_three_mem_range_expand {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [CharP R 3] : W.Φ 3 ∈ Set.range ⇑(Polynomial.expand R 3)

In characteristic three, Φ₃ is a polynomial in X³: explicitly, Φ₃ = expand 3 g for the cubic g = X³ − b₂b₄X² + (b₂²b₄² − b₂³b₆ + b₂b₄b₆)X + (b₄³b₆ − b₂b₄b₆² + b₆³).

The difference expand 3 g − Φ₃ is 3·M + N·(b₂b₆ − b₄² − b₈) for explicit polynomials M, N (computed symbolically over ℤ, entering through linear_combination), so it vanishes by CharP.cast_eq_zero and the characteristic-three b-relation WeierstrassCurve.b_relation_of_char_three.