Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_WeierstrassCurve_KernelIdeal.lean

definition module

Kernel ideals of rationally represented maps of Weierstrass curves

The setting is a field F, an extension field k of F, and Weierstrass curves over F; all curves are base changed to k and read on the k-points of the associated affine curve. The input data are two curves W_0, W over F and a homomorphism of additive groups \chi \colon W_0(k) \to W(k), with no rationality requirement imposed on \chi itself.

The module defines WeierstrassCurve.kernelIdealSet k W₀ W χ, a subset of the subring rationalEndSubring k W₀ of \mathrm{End}(W_0(k)): an element a belongs to it exactly when there is a \rho \in rationalHomSet k W W₀ such that the endomorphism underlying a is \chi followed by \rho, i.e. a = \rho \circ \chi as maps W_0(k) \to W_0(k). Here rationalHomSet k W W₀ consists of those additive maps W(k) \to W_0(k) that are either zero or rationally represented, meaning that there are four polynomials n_X, d_X, n_Y, d_Y \in F[X][Y] and a finite exceptional set B \subseteq k such that, for every nonsingular affine point (x,y) of the base change with x \notin B, the two denominators do not vanish at (x,y) after mapping the coefficients into k and the image of (x,y) is the affine point with coordinates n_X/d_X and n_Y/d_Y evaluated there; and rationalEndSubring k W₀ is the subring of \mathrm{End}(W_0(k)) generated by the rationally represented self-maps of W_0. Thus the definition is the left ideal-style set \{\rho\chi : \rho \in \mathrm{Hom}^{\mathrm{rat}}(W, W_0)\}, described as a subset rather than packaged as an ideal. Two accompanying lemmas record that 0 lies in kernelIdealSet k W₀ W χ for every \chi, and that 1 lies in kernelIdealSet k W W (AddMonoidHom.id _).

Relation to Mathlib

Mathlib provides WeierstrassCurve, its base change and the group of affine points, but has no notion of a rationally represented map of Weierstrass curves nor of kernel ideals; rationalHomSet, rationalEndSubring and kernelIdealSet are the project's own, phrased entirely in terms of additive endomorphisms of groups of k-points.

Where it is used

For k algebraically closed and \chi arising from an isogeny, this set is the kernel ideal that Deuring's and Waterhouse's theory attaches to \ker\chi inside the endomorphism ring of W_0; it provides the ideal-theoretic bookkeeping for endomorphism rings of elliptic curves in the parts of the development that analyse curves over finite fields.

References

  1. W. C. Waterhouse, Abelian varieties over finite fields, Annales scientifiques de l'École Normale Supérieure 2 (1969), 521–560
  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_KernelIdeal.lean

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_WeierstrassCurve_RationalEnd

namespace WeierstrassCurve

universe u v

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

def kernelIdealSet (W₀ W : WeierstrassCurve F)
    (χ : (W₀.baseChange k).toAffine.Point →+ (W.baseChange k).toAffine.Point) :
    Set (rationalEndSubring k W₀) :=
  {a | ∃ ρ ∈ rationalHomSet k W W₀,
    (a : AddMonoid.End (W₀.baseChange k).toAffine.Point) = ρ.comp χ}

theorem zero_mem_kernelIdealSet (W₀ W : WeierstrassCurve F)
    (χ : (W₀.baseChange k).toAffine.Point →+ (W.baseChange k).toAffine.Point) :
    (0 : rationalEndSubring k W₀) ∈ kernelIdealSet k W₀ W χ :=
  ⟨0, zero_mem_rationalHomSet k W W₀, by rw [AddMonoidHom.zero_comp]; rfl⟩

theorem one_mem_kernelIdealSet_id (W : WeierstrassCurve F) :
    (1 : rationalEndSubring k W) ∈ kernelIdealSet k W W (AddMonoidHom.id _) :=
  ⟨AddMonoidHom.id _, id_mem_rationalHomSet k W, rfl⟩

end WeierstrassCurve

Statements phrased using this module (49)