Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_WeierstrassCurve_RatPointHom.lean

definition module

Affine Weierstrass points: functoriality along a field homomorphism

Throughout, F and k are fields, f : F \to k is a ring homomorphism and W_0 is a Weierstrass curve over F; W_0.map\ f denotes the Weierstrass curve over k obtained by applying f to the coefficients. The underlying map is WeierstrassCurve.ratPointMap, defined by cases on an affine point of W_0: the point at infinity goes to the point at infinity, and an affine point (x,y) together with a proof that it is nonsingular on W_0 goes to (f(x),f(y)), the nonsingularity being transported along f by WeierstrassCurve.Affine.map_nonsingular applied to the injectivity of a ring homomorphism of fields. This module records the basic properties of that map and packages it as a homomorphism. ratPointMap_zero and ratPointMap_some are the two defining equations. Affine.Point.some_congr is a congruence lemma: two affine points Point.some x₁ y₁ h₁ and Point.some x₂ y₂ h₂ on a Weierstrass curve over k are equal as soon as x_1 = x_2 and y_1 = y_2, irrespective of the nonsingularity proofs carried. ratPointMap_injective asserts injectivity of ratPointMap f, by the injectivity of f. ratPointMap_add, stated with decidable equality on F and on k so that Mathlib's addition of affine points is available, asserts f_*(P+Q) = f_*P + f_*Q for all affine points P,Q of W_0; the proof is the expected case analysis, splitting on whether x_1 = x_2 and y_1 = -Y(x_2,y_2), and using the compatibility of f with negY, with the slope and with the addition formulae for the x- and y-coordinates. Finally ratPointHom bundles ratPointMap f as an additive monoid homomorphism W_0(F)^{\mathrm{aff}} \to (W_0.map\ f)(k)^{\mathrm{aff}} between the groups of affine points.

Relation to Mathlib

The transport of nonsingularity along f and the compatibility of f with negY, the slope and the addition formulae are Mathlib results (Affine.map_nonsingular, Affine.map_negY, Affine.map_slope, Affine.map_addX, Affine.map_addY); what is added here is the packaging of the coordinatewise map as an injective additive group homomorphism under the project's names ratPointMap and ratPointHom.

Where it is used

This is the base-change map on points used in setting up the Galois-theoretic side of the argument, for instance the inclusion E(\mathbb{Q}) \hookrightarrow E(\overline{\mathbb{Q}}) obtained by taking f to be the structure map of an algebraic closure, so that rational points may be compared with points over larger fields and with torsion subgroups carrying Galois actions.

References

  1. J. H. Silverman, The Arithmetic of Elliptic Curves, 2nd ed., Graduate Texts in Mathematics 106, Springer, 2009, Chapter III
  2. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154

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

Imports

Imported by

Declarations

Source

import Definitions.Def_WeierstrassCurve_RatPointMap_probe

set_option autoImplicit false

namespace WeierstrassCurve

open WeierstrassCurve.Affine

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

theorem Affine.Point.some_congr {V : Affine k} {x₁ y₁ x₂ y₂ : k} (hx : x₁ = x₂)
    (hy : y₁ = y₂) (h₁ : V.Nonsingular x₁ y₁) (h₂ : V.Nonsingular x₂ y₂) :
    Point.some x₁ y₁ h₁ = Point.some x₂ y₂ h₂ := by
  subst hx; subst hy; rfl

@[simp]
lemma ratPointMap_zero : ratPointMap f (0 : W₀.toAffine.Point) = 0 :=
  rfl

lemma ratPointMap_some {x y : F} (h : W₀.toAffine.Nonsingular x y) :
    ratPointMap f (.some x y h)
      = .some (f x) (f y) ((W₀.toAffine.map_nonsingular f.injective x y).mpr h) :=
  rfl

lemma ratPointMap_injective : Function.Injective (ratPointMap f (W₀ := W₀)) := by
  rintro (_ | ⟨x₁, y₁, h₁⟩) (_ | ⟨x₂, y₂, h₂⟩) h
  · rfl
  · exact absurd h.symm (Affine.Point.some_ne_zero _)
  · exact absurd h (Affine.Point.some_ne_zero _)
  · rw [ratPointMap_some, ratPointMap_some, Affine.Point.some.injEq] at h
    exact Affine.Point.some_congr (f.injective h.1) (f.injective h.2) _ _

theorem ratPointMap_add [DecidableEq F] [DecidableEq k] (P Q : W₀.toAffine.Point) :
    ratPointMap f (P + Q) = ratPointMap f P + ratPointMap f Q := by
  rcases P with _ | ⟨x₁, y₁, h₁⟩ <;> rcases Q with _ | ⟨x₂, y₂, h₂⟩
  any_goals rfl
  by_cases hxy : x₁ = x₂ ∧ y₁ = W₀.toAffine.negY x₂ y₂
  · rw [Affine.Point.add_of_Y_eq hxy.1 hxy.2, ratPointMap_zero, ratPointMap_some,
      ratPointMap_some,
      Affine.Point.add_of_Y_eq (congrArg f hxy.1) (by rw [hxy.2, Affine.map_negY])]
  · have hxy' : ¬(f x₁ = f x₂ ∧ f y₁ = (W₀.map f).toAffine.negY (f x₂) (f y₂)) := by
      rintro ⟨hx, hy⟩
      rw [Affine.map_negY] at hy
      exact hxy ⟨f.injective hx, f.injective hy⟩
    rw [Affine.Point.add_some hxy, ratPointMap_some, ratPointMap_some, ratPointMap_some,
      Affine.Point.add_some hxy']
    exact Affine.Point.some_congr (by rw [Affine.map_slope, Affine.map_addX])
      (by rw [Affine.map_slope, Affine.map_addY]) _ _

@[simps]
def ratPointHom [DecidableEq F] [DecidableEq k] :
    W₀.toAffine.Point →+ (W₀.map f).toAffine.Point where
  toFun := ratPointMap f
  map_zero' := rfl
  map_add' := ratPointMap_add f

end WeierstrassCurve

Statements phrased using this module (10)