Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_WeierstrassCurve_VeluEquivariance.lean

definition module

Base change and Galois equivariance of Vélu's formulas

This module records the naturality of the project's Vélu construction under base change of the coefficient ring, and deduces from it the Galois equivariance of the Vélu quotient and its coordinate maps.

For a Weierstrass curve W over a commutative ring R and a ring homomorphism f : R \to A, the first group of lemmas states that each per-point Vélu quantity commutes with f: evaluating g_x = 3x^2 + 2a_2x + a_4 - a_1y, g_y = -(2y + a_1x + a_3), t = 2g_x - a_1g_y = 6x^2 + b_2x + b_4, u = g_y^2 and w = u + xt on the base-changed curve W.map f at (f x, f y) gives the image under f of the corresponding value for W at (x,y). For the sums \mathrm{veluTSum} and \mathrm{veluWSum} over a finite set S \subseteq R \times R the statements are for the image of S under the embedding induced by f on each coordinate, and accordingly assume f injective; the same holds for the quotient curve, so that (\mathrm{veluQuotient}) of the base-changed curve at the image set equals the base change of W.\mathrm{veluQuotient}\,S (coefficients a_1,a_2,a_3 unchanged, a_4 - 5t_S, a_6 - b_2t_S - 7w_S). Singleton versions need no injectivity, and over fields the rational coordinate maps \mathrm{veluX}, \mathrm{veluY} for a singleton set likewise commute with a field homomorphism.

Two lemmas show that \mathrm{veluX} and \mathrm{veluY} for the singleton \{(x_0,y_0)\} are unchanged upon replacing y_0 by -y_0 - a_1x_0 - a_3, so only the x-coordinate of the chosen point matters. Combining these, for a ring endomorphism \sigma of a field F with W.\mathrm{map}\,\sigma = W, a point (x_0,y_0) satisfying the affine Weierstrass equation and \sigma x_0 = x_0, it follows that the quotient curve W.\mathrm{veluQuotient}\,\{(x_0,y_0)\} is \sigma-invariant and that \mathrm{veluX} and \mathrm{veluY} commute with \sigma; the step is that \sigma y_0 is either y_0 or its negative-Y partner.

Finally, under the hypotheses that (x_0,y_0) lies on the curve, that \Psi_3 vanishes at x_0, that the quotient curve has nonzero discriminant, and that (x_0,y_0) is nonsingular, the zero locus of the point map \mathrm{veluPointMap3} (which sends the point at infinity and every affine point with x = x_0 to zero, and (x,y) with x \neq x_0 to (\mathrm{veluX}, \mathrm{veluY})) is exactly \{0, \pm(x_0,y_0)\}.

Relation to Mathlib

Mathlib supplies the Weierstrass curve structure, base change map, the affine equation and nonsingularity predicates, affine points and the division polynomial \Psi_3; the Vélu quantities, the quotient curve and the point map are the project's own.

Where it is used

These naturality statements let the Vélu quotient by the subgroup \{0, \pm Q\} generated by a 3-torsion point, together with its coordinate maps, be recognised as defined over the base field whenever the x-coordinate of Q is fixed, which is what is needed to treat 3-isogenies of elliptic curves over number fields as morphisms over the base.

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, The Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 106, Springer, 2nd edition, 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_WeierstrassCurve_VeluEquivariance.lean

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_WeierstrassCurve_VeluBundledMap

open Polynomial

namespace WeierstrassCurve

section BaseChange

variable {R : Type*} {A : Type*} [CommRing R] [CommRing A] (W : WeierstrassCurve R) (f : R →+* A)

local macro "map_simp" : tactic =>
  `(tactic| simp only [map_ofNat, map_neg, map_add, map_sub, map_mul, map_pow])

@[simp] lemma map_veluGx (x y : R) :
    (W.map f).veluGx (f x) (f y) = f (W.veluGx x y) := by
  simp only [veluGx, map_a₁, map_a₂, map_a₄]
  map_simp

@[simp] lemma map_veluGy (x y : R) :
    (W.map f).veluGy (f x) (f y) = f (W.veluGy x y) := by
  simp only [veluGy, map_a₁, map_a₃]
  map_simp

@[simp] lemma map_veluT (x y : R) :
    (W.map f).veluT (f x) (f y) = f (W.veluT x y) := by
  simp only [veluT_eq, map_b₂, map_b₄]
  map_simp

@[simp] lemma map_veluU (x y : R) :
    (W.map f).veluU (f x) (f y) = f (W.veluU x y) := by
  simp only [veluU, map_veluGy, map_pow]

@[simp] lemma map_veluW (x y : R) :
    (W.map f).veluW (f x) (f y) = f (W.veluW x y) := by
  simp only [veluW, map_veluU, map_veluT, map_add, map_mul]

lemma map_veluTSum (S : Finset (R × R)) (hf : Function.Injective f) :
    (W.map f).veluTSum (S.map ⟨Prod.map f f, hf.prodMap hf⟩) = f (W.veluTSum S) := by
  rw [veluTSum, veluTSum, Finset.sum_map, map_sum]
  exact Finset.sum_congr rfl fun P _ => by
    simp only [Function.Embedding.coeFn_mk, Prod.map_fst, Prod.map_snd, map_veluT]

lemma map_veluWSum (S : Finset (R × R)) (hf : Function.Injective f) :
    (W.map f).veluWSum (S.map ⟨Prod.map f f, hf.prodMap hf⟩) = f (W.veluWSum S) := by
  rw [veluWSum, veluWSum, Finset.sum_map, map_sum]
  exact Finset.sum_congr rfl fun P _ => by
    simp only [Function.Embedding.coeFn_mk, Prod.map_fst, Prod.map_snd, map_veluW]

@[simp] lemma map_veluTSum_singleton (x₀ y₀ : R) :
    (W.map f).veluTSum {(f x₀, f y₀)} = f (W.veluTSum {(x₀, y₀)}) := by
  simp only [veluTSum, Finset.sum_singleton, map_veluT]

@[simp] lemma map_veluWSum_singleton (x₀ y₀ : R) :
    (W.map f).veluWSum {(f x₀, f y₀)} = f (W.veluWSum {(x₀, y₀)}) := by
  simp only [veluWSum, Finset.sum_singleton, map_veluW]

lemma map_veluQuotient (S : Finset (R × R)) (hf : Function.Injective f) :
    (W.map f).veluQuotient (S.map ⟨Prod.map f f, hf.prodMap hf⟩) = (W.veluQuotient S).map f := by
  ext
  · simp [veluQuotient]
  · simp [veluQuotient]
  · simp [veluQuotient]
  · simp only [veluQuotient_a₄, map_a₄, map_veluTSum _ _ S hf]
    map_simp
  · simp only [veluQuotient_a₆, map_a₆, map_b₂, map_veluTSum _ _ S hf, map_veluWSum _ _ S hf]
    map_simp

lemma map_veluQuotient_singleton (x₀ y₀ : R) :
    (W.map f).veluQuotient {(f x₀, f y₀)} = (W.veluQuotient {(x₀, y₀)}).map f := by
  ext
  · simp [veluQuotient]
  · simp [veluQuotient]
  · simp [veluQuotient]
  · simp only [veluQuotient_a₄, map_a₄, map_veluTSum_singleton]
    map_simp
  · simp only [veluQuotient_a₆, map_a₆, map_b₂, map_veluTSum_singleton, map_veluWSum_singleton]
    map_simp

end BaseChange

section FieldBaseChange

variable {F F' : Type*} [Field F] [Field F'] (W : WeierstrassCurve F) (f : F →+* F')

lemma map_veluX_singleton (x₀ y₀ x : F) :
    (W.map f).veluX {(f x₀, f y₀)} (f x) = f (W.veluX {(x₀, y₀)} x) := by
  simp only [veluX, Finset.sum_singleton, map_veluT, map_veluU, map_add, map_div₀, map_sub,
    map_pow]

lemma map_veluY_singleton (x₀ y₀ x y : F) :
    (W.map f).veluY {(f x₀, f y₀)} (f x) (f y) = f (W.veluY {(x₀, y₀)} x y) := by
  simp only [veluY, Finset.sum_singleton, map_veluT, map_veluU, map_veluGx, map_veluGy,
    map_a₁, map_a₃, map_add, map_sub, map_mul, map_div₀, map_pow, map_ofNat]

end FieldBaseChange

section Representative

variable {F : Type*} [Field F] (W : WeierstrassCurve F)

lemma veluX_singleton_negY (x₀ y₀ x : F) :
    W.veluX {(x₀, W.toAffine.negY x₀ y₀)} x = W.veluX {(x₀, y₀)} x := by
  simp only [veluX, Finset.sum_singleton, veluT_negY, veluU_negY]

lemma veluY_singleton_negY (x₀ y₀ x y : F) :
    W.veluY {(x₀, W.toAffine.negY x₀ y₀)} x y = W.veluY {(x₀, y₀)} x y := by
  rcases eq_or_ne x x₀ with h | h
  · subst h
    simp [veluY, sub_self]
  · have hd : x - x₀ ≠ 0 := sub_ne_zero.mpr h
    simp only [veluY, Finset.sum_singleton, veluT, veluU, veluGx, veluGy, Affine.negY]
    field_simp
    ring

end Representative

section Galois

variable {F : Type*} [Field F] {W : WeierstrassCurve F} {σ : F →+* F}

private lemma sigma_y₀_eq_or_eq_negY (hW : W.map σ = W) {x₀ y₀ : F}
    (hQ : W.toAffine.Equation x₀ y₀) (hx₀ : σ x₀ = x₀) :
    σ y₀ = y₀ ∨ σ y₀ = W.toAffine.negY x₀ y₀ := by
  have h1 : (W.map σ).toAffine.Equation (σ x₀) (σ y₀) := Affine.Equation.map σ hQ
  rw [hW, hx₀] at h1
  exact Affine.Y_eq_of_X_eq h1 hQ rfl

theorem veluQuotient_singleton_map_self (hW : W.map σ = W) {x₀ y₀ : F}
    (hQ : W.toAffine.Equation x₀ y₀) (hx₀ : σ x₀ = x₀) :
    (W.veluQuotient {(x₀, y₀)}).map σ = W.veluQuotient {(x₀, y₀)} := by
  have h := W.map_veluQuotient_singleton σ x₀ y₀
  rw [hW, hx₀] at h
  rcases sigma_y₀_eq_or_eq_negY hW hQ hx₀ with hy | hy
  · rw [hy] at h
    exact h.symm
  · rw [hy] at h
    exact h.symm.trans (W.veluQuotient_singleton_negY x₀ y₀)

theorem veluX_singleton_map_comm (hW : W.map σ = W) {x₀ y₀ : F}
    (hQ : W.toAffine.Equation x₀ y₀) (hx₀ : σ x₀ = x₀) (x : F) :
    W.veluX {(x₀, y₀)} (σ x) = σ (W.veluX {(x₀, y₀)} x) := by
  have h := W.map_veluX_singleton σ x₀ y₀ x
  rw [hW, hx₀] at h
  rcases sigma_y₀_eq_or_eq_negY hW hQ hx₀ with hy | hy
  · rw [hy] at h
    exact h
  · rw [hy] at h
    exact (W.veluX_singleton_negY x₀ y₀ (σ x)).symm.trans h

theorem veluY_singleton_map_comm (hW : W.map σ = W) {x₀ y₀ : F}
    (hQ : W.toAffine.Equation x₀ y₀) (hx₀ : σ x₀ = x₀) (x y : F) :
    W.veluY {(x₀, y₀)} (σ x) (σ y) = σ (W.veluY {(x₀, y₀)} x y) := by
  have h := W.map_veluY_singleton σ x₀ y₀ x y
  rw [hW, hx₀] at h
  rcases sigma_y₀_eq_or_eq_negY hW hQ hx₀ with hy | hy
  · rw [hy] at h
    exact h
  · rw [hy] at h
    exact (W.veluY_singleton_negY x₀ y₀ (σ x) (σ y)).symm.trans h

end Galois

section Kernel

variable {F : Type*} [Field F] {W : WeierstrassCurve F}
variable {x₀ y₀ : F} (hQ : W.toAffine.Equation x₀ y₀) (hΨ : (W.Ψ₃).eval x₀ = 0)
  (hΔ : (W.veluQuotient {(x₀, y₀)}).Δ ≠ 0)

theorem veluPointMap3_eq_zero_iff (hQns : W.toAffine.Nonsingular x₀ y₀)
    (P : W.toAffine.Point) :
    veluPointMap3 hQ hΨ hΔ P = 0 ↔
      P = 0 ∨ P = .some x₀ y₀ hQns ∨ P = -.some x₀ y₀ hQns := by
  cases P with
  | zero =>
    constructor
    · intro _
      exact Or.inl rfl
    · intro _
      rfl
  | some x y h =>
    by_cases hx : x = x₀
    · rw [veluPointMap3_some_of_eq hQ hΨ hΔ h hx]
      constructor
      · intro _
        exact Or.inr (Affine.Point.X_eq_iff.mp hx)
      · intro _
        rfl
    · rw [veluPointMap3_some_of_ne hQ hΨ hΔ h hx]
      constructor
      · intro hcontra
        exact absurd hcontra (Affine.Point.some_ne_zero _)
      · rintro (h0 | hQ' | hQ'')
        · exact absurd h0 (Affine.Point.some_ne_zero h)
        · exact absurd (Affine.Point.X_eq_iff.mpr (Or.inl hQ')) hx
        · exact absurd (Affine.Point.X_eq_iff.mpr (Or.inr hQ'')) hx

end Kernel

end WeierstrassCurve

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).