Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_KatzLevelPQuotient.lean

definition module

Vélu quotient of a Weierstrass curve by a torsion line

Over a commutative ring A with a Weierstrass curve W\colon y^2+a_1xy+a_3y=x^3+a_2x^2+a_4x+a_6, the module builds the Vélu quotient of W by the line generated by a point, written purely in terms of the x-coordinate. First, for a\in\mathbb Z and x\in A, smulX W a x is (\Phi_a)(x)\cdot\mathrm{inv}\bigl((\Psi^{\mathrm{Sq}}_a)(x)\bigr), formed with Mathlib's division polynomials and Ring.inverse; it is therefore a total function of x, and is the x-coordinate of [a]Q exactly when (\Psi^{\mathrm{Sq}}_a)(x) is a unit. The accompanying lemmas record \mathrm{smulX}(a,x)\cdot(\Psi^{\mathrm{Sq}}_a)(x)=(\Phi_a)(x) under that unit hypothesis, \mathrm{smulX}(1,x)=x, and compatibility with a ring homomorphism f\colon A\to B (again under the unit hypothesis).

For p\in\mathbb N and x\in A, put x_a:=\mathrm{smulX}(a,x) and define t:=\sum_{a=1}^{(p-1)/2}(6x_a^2+b_2x_a+b_4) (veluTLine) and w:=\sum_{a=1}^{(p-1)/2}\bigl(\Psi_2^{\mathrm{Sq}}(x_a)+x_a(6x_a^2+b_2x_a+b_4)\bigr) (veluWLine), the index running over the natural numbers in [1,(p-1)/2] with truncated subtraction and division. Then quotientByLine W p x is the Weierstrass curve with the same a_1,a_2,a_3 and with a_4-5t, a_6-b_2t-7w; it is a bare Weierstrass presentation, not an isogeny or a quotient scheme. Its invariants are computed: b_2'=b_2, b_4'=b_4-10t, b_6'=b_6-4b_2t-28w. For p\le 2 the index set is empty and the construction returns W; and it commutes with base change along f provided each (\Psi^{\mathrm{Sq}}_a)(x), 1\le a\le (p-1)/2, is a unit. Finally, for level-p data D=(x_P,y_P,x_Q,y_Q), quotientBySndLine and quotientByFstLine apply this at x_Q and at x_P respectively, and the swap of D interchanges the two.

Relation to Mathlib

Mathlib supplies the Weierstrass curve structure, its b- and c-invariants, base change, and the division polynomials \Phi_a, \Psi^{\mathrm{Sq}}_a, \Psi_2^{\mathrm{Sq}} used here; the Vélu quotient curve itself, in this x-coordinate-only form valid over an arbitrary commutative ring, is the project's own.

Where it is used

The quotient curve attached to level-p data is what is needed to define the degeneracy and Hecke-type operators on the project's Katz modular forms of level p, whose Weierstrass-curve-valued definition requires a construction of the quotient that is functorial in the base ring.

References

  1. J. Vélu, Isogénies entre courbes elliptiques, C. R. Acad. Sci. Paris Sér. A 273 (1971), 238–241
  2. J. H. Silverman, The Arithmetic of Elliptic Curves, 2nd edition, Graduate Texts in Mathematics 106, Springer, 2009

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_ModularCurve_KatzLevelPQuotient.lean

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_KatzLevelP

set_option autoImplicit false

noncomputable section

open WeierstrassCurve Polynomial

namespace ModularCurve

namespace LevelP

variable {A B : Type*} [CommRing A] [CommRing B] (W : WeierstrassCurve A)

def smulX (a : ℤ) (x : A) : A :=
  (W.Φ a).eval x * Ring.inverse ((W.ΨSq a).eval x)

theorem smulX_mul_ΨSq {a : ℤ} {x : A} (h : IsUnit ((W.ΨSq a).eval x)) :
    smulX W a x * (W.ΨSq a).eval x = (W.Φ a).eval x := by
  rw [smulX, mul_assoc, Ring.inverse_mul_cancel _ h, mul_one]

@[simp] theorem smulX_one (x : A) : smulX W 1 x = x := by
  simp [smulX, WeierstrassCurve.Φ_one, WeierstrassCurve.ΨSq_one]

theorem map_smulX (f : A →+* B) {a : ℤ} {x : A} (h : IsUnit ((W.ΨSq a).eval x)) :
    f (smulX W a x) = smulX (W.map f) a (f x) := by
  obtain ⟨u, hu⟩ := h
  rw [smulX, smulX, WeierstrassCurve.map_Φ, WeierstrassCurve.map_ΨSq, Polynomial.eval_map,
    Polynomial.eval_map, Polynomial.eval₂_at_apply, Polynomial.eval₂_at_apply, map_mul, ← hu,
    Ring.inverse_unit]
  change _ = _ * Ring.inverse ((Units.map (f : A →* B) u : Bˣ) : B)
  rw [Ring.inverse_unit]
  rfl

variable (p : ℕ)

def veluTLine (x : A) : A :=
  ∑ a ∈ Finset.Icc 1 ((p - 1) / 2), (6 * smulX W a x ^ 2 + W.b₂ * smulX W a x + W.b₄)

def veluWLine (x : A) : A :=
  ∑ a ∈ Finset.Icc 1 ((p - 1) / 2),
    (W.Ψ₂Sq.eval (smulX W a x) + smulX W a x * (6 * smulX W a x ^ 2 + W.b₂ * smulX W a x + W.b₄))

def quotientByLine (x : A) : WeierstrassCurve A where
  a₁ := W.a₁
  a₂ := W.a₂
  a₃ := W.a₃
  a₄ := W.a₄ - 5 * veluTLine W p x
  a₆ := W.a₆ - W.b₂ * veluTLine W p x - 7 * veluWLine W p x

variable (x : A)

@[simp] theorem quotientByLine_a₁ : (quotientByLine W p x).a₁ = W.a₁ := rfl
@[simp] theorem quotientByLine_a₂ : (quotientByLine W p x).a₂ = W.a₂ := rfl
@[simp] theorem quotientByLine_a₃ : (quotientByLine W p x).a₃ = W.a₃ := rfl
theorem quotientByLine_a₄ : (quotientByLine W p x).a₄ = W.a₄ - 5 * veluTLine W p x := rfl
theorem quotientByLine_a₆ :
    (quotientByLine W p x).a₆ = W.a₆ - W.b₂ * veluTLine W p x - 7 * veluWLine W p x := rfl

theorem quotientByLine_b₂ : (quotientByLine W p x).b₂ = W.b₂ := by
  simp [WeierstrassCurve.b₂]

theorem quotientByLine_b₄ : (quotientByLine W p x).b₄ = W.b₄ - 10 * veluTLine W p x := by
  simp only [WeierstrassCurve.b₄, quotientByLine_a₁, quotientByLine_a₃, quotientByLine_a₄]; ring

theorem quotientByLine_b₆ :
    (quotientByLine W p x).b₆ = W.b₆ - 4 * W.b₂ * veluTLine W p x - 28 * veluWLine W p x := by
  simp only [WeierstrassCurve.b₆, WeierstrassCurve.b₂, quotientByLine_a₃, quotientByLine_a₆]; ring

theorem quotientByLine_of_le_two (hp : p ≤ 2) : quotientByLine W p x = W := by
  have h0 : (p - 1) / 2 = 0 := by omega
  ext <;> simp [quotientByLine, veluTLine, veluWLine, h0]

theorem quotientByLine_map (f : A →+* B)
    (h : ∀ a ∈ Finset.Icc 1 ((p - 1) / 2), IsUnit ((W.ΨSq a).eval x)) :
    (quotientByLine W p x).map f = quotientByLine (W.map f) p (f x) := by
  have hT : f (veluTLine W p x) = veluTLine (W.map f) p (f x) := by
    simp only [veluTLine, map_sum]
    refine Finset.sum_congr rfl fun a ha => ?_
    rw [map_add, map_add, map_mul, map_mul, map_pow, map_smulX W f (h a ha), WeierstrassCurve.map_b₂,
      WeierstrassCurve.map_b₄, map_ofNat]
  have hW : f (veluWLine W p x) = veluWLine (W.map f) p (f x) := by
    simp only [veluWLine, map_sum]
    refine Finset.sum_congr rfl fun a ha => ?_
    have hx := map_smulX W f (h a ha)
    simp only [map_add, map_mul, map_pow, hx, WeierstrassCurve.map_b₂, WeierstrassCurve.map_b₄,
      map_ofNat, WeierstrassCurve.Ψ₂Sq, WeierstrassCurve.map_b₆, eval_add, eval_mul, eval_pow,
      eval_C, eval_X, eval_ofNat]
  ext
  · simp [quotientByLine]
  · simp [quotientByLine]
  · simp [quotientByLine]
  · simp [quotientByLine, hT, map_ofNat]
  · simp [quotientByLine, hT, hW, map_ofNat]

end LevelP

namespace LevelPData

variable {A : Type*} [CommRing A] (W : WeierstrassCurve A) (p : ℕ) (D : LevelPData A)

def quotientBySndLine : WeierstrassCurve A := LevelP.quotientByLine W p D.xQ

def quotientByFstLine : WeierstrassCurve A := LevelP.quotientByLine W p D.xP

@[simp] theorem quotientBySndLine_swap : D.swap.quotientBySndLine W p = D.quotientByFstLine W p := rfl

@[simp] theorem quotientByFstLine_swap : D.swap.quotientByFstLine W p = D.quotientBySndLine W p := rfl

theorem quotientBySndLine_eq : D.quotientBySndLine W p = LevelP.quotientByLine W p D.xQ := rfl

theorem quotientByFstLine_eq : D.quotientByFstLine W p = LevelP.quotientByLine W p D.xP := rfl

end LevelPData

end ModularCurve

end

Statements phrased using this module (5)