Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_TateVeluRingTwo.lean

definition module

Vélu order-two coordinate maps over commutative rings

For a Weierstrass curve W over a commutative ring A, with g_x(x_0,y_0) = 3x_0^2 + 2a_2x_0 + a_4 - a_1y_0 denoting WeierstrassCurve.veluGx, two coordinate functions are defined by the order-two Vélu formulas, written with Ring.inverse in place of division so that they make sense over any commutative ring: velu2XR sends x to x + g_x(x_0,y_0)\cdot(x-x_0)^{-1} and velu2YR sends (x,y) to y - g_x(x_0,y_0)\,\bigl(a_1(x-x_0)+y-y_0\bigr)\cdot\bigl((x-x_0)^{-1}\bigr)^2, where (x-x_0)^{-1} means Ring.inverse (x - x₀) (the two-sided inverse when x-x_0 is a unit, and 0 otherwise). Over a field F these agree, for all values of the arguments, with the division-based WeierstrassCurve.velu2X and WeierstrassCurve.velu2Y (velu2XR_eq_velu2X, velu2YR_eq_velu2Y), since Ring.inverse coincides with field inversion there.

The remaining statements are naturality assertions for a ring homomorphism f : A \to B. For x_0,y_0,x,y \in A with x - x_0 a unit in A, one has f(\mathrm{velu2XR}\,W\,x_0\,y_0\,x) = \mathrm{velu2XR}\,(W.\mathrm{map}\,f)\,(f x_0)\,(f y_0)\,(f x) and likewise for the y-coordinate (map_velu2XR, map_velu2YR); the unit hypothesis is what licenses pushing Ring.inverse through f. Finally, map_veluQuotient2 states that Vélu's order-two quotient curve is compatible with base change: the Weierstrass curve (W.\mathrm{veluQuotient2}\,x_0\,y_0).\mathrm{map}\,f equals (W.\mathrm{map}\,f).\mathrm{veluQuotient2}\,(f x_0)\,(f y_0), i.e. the coefficients a_1,a_2,a_3, a_4 - 5g_x(x_0,y_0) and a_6 - b_2 g_x(x_0,y_0) - 7x_0 g_x(x_0,y_0) are carried to the corresponding coefficients over B. No assertion about points or equations of curves is made here: the content is the formulas and their functoriality.

Relation to Mathlib

Mathlib supplies WeierstrassCurve, its base-change map and Ring.inverse; the Vélu coordinate maps and the order-two quotient curve WeierstrassCurve.veluQuotient2 are the project's own definitions, and these are their Ring.inverse-valued versions over a general commutative ring.

Where it is used

These ring-level formulas allow the order-two Vélu isogeny identities for the Tate curve and its torus points, established over a field, to be transported along ring homomorphisms, in particular from a characteristic-zero cyclotomic base to its quotients; they are used in the modules treating Tate-curve level structures and cusps.

References

  1. J. Vélu, Isogénies entre courbes elliptiques, C. R. Acad. Sci. Paris Sér. A-B 273 (1971), 238–241
  2. J. H. Silverman, Advanced Topics in the Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 151, Springer, 1994, Chapter V

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_TateVeluRingTwo.lean

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_TateVeluRing
import Definitions.Def_WeierstrassCurve_VeluOrderTwo
import Definitions.Def_WeierstrassCurve_VeluPointMap2

set_option autoImplicit false

noncomputable section

open ModularCurve WeierstrassCurve

namespace ModularCurve.TateVeluRing

section Velu2R

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

noncomputable def velu2XR (x₀ y₀ x : A) : A := x + W.veluGx x₀ y₀ * Ring.inverse (x - x₀)

noncomputable def velu2YR (x₀ y₀ x y : A) : A :=
  y - W.veluGx x₀ y₀ * (W.a₁ * (x - x₀) + y - y₀) * Ring.inverse (x - x₀) ^ 2

theorem velu2XR_eq_velu2X {F : Type*} [Field F] (W : WeierstrassCurve F) (x₀ y₀ x : F) :
    velu2XR W x₀ y₀ x = W.velu2X x₀ y₀ x := by
  unfold velu2XR WeierstrassCurve.velu2X
  simp only [Ring.inverse_eq_inv', div_eq_mul_inv]

theorem velu2YR_eq_velu2Y {F : Type*} [Field F] (W : WeierstrassCurve F) (x₀ y₀ x y : F) :
    velu2YR W x₀ y₀ x y = W.velu2Y x₀ y₀ x y := by
  unfold velu2YR WeierstrassCurve.velu2Y
  simp only [Ring.inverse_eq_inv', div_eq_mul_inv, inv_pow]

variable {B : Type*} [CommRing B] (f : A →+* B)

theorem map_velu2XR (x₀ y₀ x : A) (hunit : IsUnit (x - x₀)) :
    f (velu2XR W x₀ y₀ x) = velu2XR (W.map f) (f x₀) (f y₀) (f x) := by
  unfold velu2XR
  have h := map_ringInverse_of_isUnit f hunit
  rw [map_sub] at h
  simp only [map_veluGx, map_add, map_mul, h]

theorem map_velu2YR (x₀ y₀ x y : A) (hunit : IsUnit (x - x₀)) :
    f (velu2YR W x₀ y₀ x y) = velu2YR (W.map f) (f x₀) (f y₀) (f x) (f y) := by
  unfold velu2YR
  have h := map_ringInverse_of_isUnit f hunit
  rw [map_sub] at h
  simp only [map_veluGx, WeierstrassCurve.map_a₁, map_add, map_sub, map_mul, map_pow, h]

theorem map_veluQuotient2 (x₀ y₀ : A) :
    (W.veluQuotient2 x₀ y₀).map f = (W.map f).veluQuotient2 (f x₀) (f y₀) := by
  ext
  · rfl
  · rfl
  · rfl
  · simp only [WeierstrassCurve.map_a₄, WeierstrassCurve.veluQuotient2_a₄, map_sub, map_mul, map_ofNat, map_veluGx]
  · simp only [WeierstrassCurve.map_a₆, WeierstrassCurve.veluQuotient2_a₆, WeierstrassCurve.map_b₂, map_sub, map_mul,
      map_ofNat, map_veluGx]

end Velu2R

end ModularCurve.TateVeluRing

end

Statements phrased using this module (1)