Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_WeierstrassCurve_RationalEnd.lean

definition module

Rationally represented homomorphisms; rational endomorphism subring

Fix a field F, an F-algebra k which is again a field, and Weierstrass curves over F. The helper WeierstrassCurve.evalEvalBC k p x y takes p \in F[X][Y], pushes its coefficients along F \to k (via mapRingHom (algebraMap F k)) and evaluates the result at the inner variable x and the outer variable y, giving the value p(x,y) \in k.

The central predicate IsRationallyRepresented k W₁ W₂ α, for an additive homomorphism \alpha from the group of affine points of W₁.baseChange k to that of W₂.baseChange k, asserts the existence of four polynomials n_X, d_X, n_Y, d_Y \in F[X][Y] and a finite subset B \subseteq k such that for every nonsingular affine point (x,y) of W_1 over k whose abscissa satisfies x \notin B, one has d_X(x,y) \neq 0, d_Y(x,y) \neq 0, and \alpha sends that point to the affine point with coordinates \bigl(n_X(x,y)/d_X(x,y),\, n_Y(x,y)/d_Y(x,y)\bigr) — in particular \alpha is required to take an affine, not infinite, value there, and a nonsingularity witness for the image is part of the existential. Note that the exceptional set is a set of x-coordinates only.

Then rationalHomSet k W₁ W₂ is the set of additive homomorphisms that are either identically zero or rationally represented in this sense (a plain union, with no group or ring structure asserted), and rationalEndSubring k W is the subring of the ring AddMonoid.End of the k-points of W.baseChange k (multiplication being composition) generated by rationalHomSet k W W.

The accompanying lemmas record that 0 lies in rationalHomSet; that the identity is rationally represented by the quadruple (X, 1, Y, 1) with B = \varnothing, hence lies in rationalHomSet and the unit lies in rationalEndSubring; and that if \sigma : k \to k is an F-algebra map with \sigma(x) = x^q for all x, then the induced map on points is rationally represented by (X^q, 1, Y^q, 1) with B = \varnothing, so it lies in rationalEndSubring k W.

Relation to Mathlib

Mathlib supplies the ambient notions used here — WeierstrassCurve, baseChange, the group of affine points toAffine.Point, the functorial point map Affine.Point.map, and bivariate evaluation evalEval — but has no notion of isogeny, rational map or endomorphism ring of a Weierstrass curve; the predicate on homomorphisms of groups of k-points and the generated subring of AddMonoid.End are the project's own.

Where it is used

These definitions give the project a concrete, elementary substitute for \mathrm{Hom}_F(W_1,W_2) and \mathrm{End}_F(W): rationality is expressed by a quadruple of polynomials over F representing the map on all but finitely many abscissae, so that, for instance, the q-power Frobenius of a curve over a finite field is available as an element of the endomorphism subring. They are intended for use with k algebraically closed, where this set coincides with the image of the genuine F-rational homomorphisms.

References

  1. J. H. Silverman, The Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 106, Springer, 1986, Chapter III, §4
  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_RationalEnd.lean

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

noncomputable section

open Polynomial
open scoped Polynomial.Bivariate

namespace WeierstrassCurve

universe u v

variable {F : Type u} [Field F] (k : Type v) [Field k] [Algebra F k]

def evalEvalBC (p : F[X][Y]) (x y : k) : k :=
  (p.map (mapRingHom (algebraMap F k))).evalEval x y

variable [DecidableEq k]

def IsRationallyRepresented (W₁ W₂ : WeierstrassCurve F)
    (α : (W₁.baseChange k).toAffine.Point →+ (W₂.baseChange k).toAffine.Point) : Prop :=
  ∃ (nX dX nY dY : F[X][Y]) (B : Set k), B.Finite ∧
    ∀ (x y : k) (h : (W₁.baseChange k).toAffine.Nonsingular x y), x ∉ B →
      evalEvalBC k dX x y ≠ 0 ∧ evalEvalBC k dY x y ≠ 0 ∧
        ∃ h', α (.some x y h) =
          .some (evalEvalBC k nX x y / evalEvalBC k dX x y)
            (evalEvalBC k nY x y / evalEvalBC k dY x y) h'

def rationalHomSet (W₁ W₂ : WeierstrassCurve F) :
    Set ((W₁.baseChange k).toAffine.Point →+ (W₂.baseChange k).toAffine.Point) :=
  {α | α = 0 ∨ IsRationallyRepresented k W₁ W₂ α}

def rationalEndSubring (W : WeierstrassCurve F) :
    Subring (AddMonoid.End (W.baseChange k).toAffine.Point) :=
  Subring.closure (rationalHomSet k W W)

theorem zero_mem_rationalHomSet (W₁ W₂ : WeierstrassCurve F) :
    (0 : (W₁.baseChange k).toAffine.Point →+ (W₂.baseChange k).toAffine.Point) ∈
      rationalHomSet k W₁ W₂ :=
  Or.inl rfl

theorem isRationallyRepresented_id (W : WeierstrassCurve F) :
    IsRationallyRepresented k W W (AddMonoidHom.id _) := by
  refine ⟨C X, 1, X, 1, ∅, Set.finite_empty, fun x y h _ => ?_⟩
  simp only [evalEvalBC, Polynomial.map_one, Polynomial.map_X, Polynomial.map_C, Polynomial.coe_mapRingHom,
    evalEval_one, evalEval_C, eval_X, evalEval_X, ne_eq, one_ne_zero, not_false_eq_true, div_one,
    AddMonoidHom.id_apply, true_and]
  exact ⟨h, trivial⟩

theorem isRationallyRepresented_map_of_pow (W : WeierstrassCurve F) (σ : k →ₐ[F] k) (q : ℕ)
    (hσ : ∀ x, σ x = x ^ q) :
    IsRationallyRepresented k W W (Affine.Point.map (W' := W) σ) := by
  refine ⟨C (X ^ q), 1, X ^ q, 1, ∅, Set.finite_empty, fun x y h _ => ?_⟩
  have e0 : evalEvalBC k (1 : F[X][Y]) x y = 1 := by
    simp [evalEvalBC, Polynomial.evalEval]
  have e1 : evalEvalBC k (C (X ^ q) : F[X][Y]) x y / evalEvalBC k (1 : F[X][Y]) x y = σ x := by
    simp [evalEvalBC, Polynomial.evalEval, hσ]
  have e2 : evalEvalBC k (X ^ q : F[X][Y]) x y / evalEvalBC k (1 : F[X][Y]) x y = σ y := by
    simp [evalEvalBC, Polynomial.evalEval, hσ]
  refine ⟨by rw [e0]; exact one_ne_zero, by rw [e0]; exact one_ne_zero, ?_⟩
  suffices H : ∀ a b : k, a = σ x → b = σ y →
      ∃ h', Affine.Point.map (W' := W) σ (.some x y h) = .some a b h' from H _ _ e1 e2
  rintro a b rfl rfl
  exact ⟨_, Affine.Point.map_some σ h⟩

theorem map_mem_rationalEndSubring_of_pow (W : WeierstrassCurve F) (σ : k →ₐ[F] k) (q : ℕ)
    (hσ : ∀ x, σ x = x ^ q) :
    (Affine.Point.map (W' := W) σ : AddMonoid.End (W.baseChange k).toAffine.Point) ∈
      rationalEndSubring k W :=
  Subring.subset_closure (Or.inr (isRationallyRepresented_map_of_pow k W σ q hσ))

theorem one_mem_rationalEndSubring (W : WeierstrassCurve F) :
    (1 : AddMonoid.End (W.baseChange k).toAffine.Point) ∈ rationalEndSubring k W :=
  Subring.one_mem _

theorem id_mem_rationalHomSet (W : WeierstrassCurve F) :
    (AddMonoidHom.id _ : (W.baseChange k).toAffine.Point →+ (W.baseChange k).toAffine.Point) ∈
      rationalHomSet k W W :=
  Or.inr (isRationallyRepresented_id k W)

end WeierstrassCurve

end

Statements phrased using this module (157)

… and 7 more statements (search for the module name to find them).