Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_EllipticCurve_FrobeniusEndo.lean

definition module

Frobenius endomorphism, endomorphism pencils, kernel degrees

For an additive commutative group A and an additive endomorphism \psi of A, FrobeniusEndo.linePencil ψ m n is, for integers m,n, the additive endomorphism P \mapsto m\cdot P - n\cdot\psi(P) of A (written as the difference m\bullet\mathrm{id}_A - n\bullet\psi in the group of additive endomorphisms); linePencil_apply records its value on a point, and mem_ker_linePencil_iff says that P lies in its kernel exactly when m\cdot P = n\cdot\psi(P). The accompanying numerical invariant FrobeniusEndo.kerDeg ψ m n is defined as Nat.card of the kernel of this pencil, i.e. the number of elements of \ker(m - n\psi), with the usual convention that it is 0 when that kernel is infinite; kerDeg_def restates the definition.

The second group of definitions applies this to a Weierstrass curve. The standing context is a tower R \to S \to k of commutative rings with k a field, a Weierstrass curve W over R, and an S-algebra automorphism \sigma of k. Here \sigma acts on the group of affine points (W⁄k).Point by applying \sigma to coordinates, and FrobeniusEndo.frobEnd W σ is this action viewed as an additive endomorphism P \mapsto \sigma\cdot P of (W⁄k).Point, with frobEnd_apply recording that value. For a natural number p, FrobeniusEndo.frobPencilEnd W σ p m n is the \mathbb{Z}/p-linear endomorphism \bar m\cdot 1 - \bar n\cdot\rho(\sigma) of the p-torsion submodule \{P : p\cdot P = 0\} of (W⁄k).Point, where \rho(\sigma) is the endomorphism induced by \sigma (the value at \sigma of galoisRepModuleEnd S W p) and \bar m, \bar n are the images of m,n in \mathbb{Z}/p. Finally, FrobeniusEndo.FrobCharEqOnPoints W σ a q is the predicate, for an integer a and a natural number q, that every point P of (W⁄k).Point satisfies \sigma(\sigma P) - a\cdot\sigma P + q\cdot P = 0: the characteristic equation of \sigma asserted pointwise on the group of points, rather than as an identity in a ring of endomorphisms.

Relation to Mathlib

Mathlib has no notion of a pencil m - n\psi of additive endomorphisms, of its kernel count, or of a pointwise characteristic equation for a field automorphism acting on the points of a Weierstrass curve; these are the project's own. The endomorphism frobEnd is the project's action of S-algebra automorphisms of k on (W⁄k).Point packaged through Mathlib's DistribSMul.toAddMonoidHom.

Where it is used

These notions provide the vocabulary for counting points and for identifying the trace and determinant of the action of a Frobenius automorphism on the p-torsion of a Weierstrass curve, which is what enters the description of the mod p Galois representation attached to the Frey curve.

References

  1. L. C. Washington, Elliptic Curves: Number Theory and Cryptography, 2nd edition, Chapman & Hall/CRC, 2008, §4.2
  2. J. H. Silverman, The Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 106, Springer, 1986, 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_EllipticCurve_FrobeniusEndo.lean

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_FLTPrelim_GaloisRep
import Definitions.Def_EllipticCurve_FrobeniusTrace

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point

noncomputable section

namespace FrobeniusEndo

section Pencil

variable {A : Type*} [AddCommGroup A]

def linePencil (ψ : A →+ A) (m n : ℤ) : A →+ A :=
  m • AddMonoidHom.id A - n • ψ

@[simp] lemma linePencil_apply (ψ : A →+ A) (m n : ℤ) (P : A) :
    linePencil ψ m n P = m • P - n • ψ P :=
  rfl

def kerDeg (ψ : A →+ A) (m n : ℤ) : ℕ :=
  Nat.card (linePencil ψ m n).ker

lemma kerDeg_def (ψ : A →+ A) (m n : ℤ) : kerDeg ψ m n = Nat.card (linePencil ψ m n).ker :=
  rfl

lemma mem_ker_linePencil_iff (ψ : A →+ A) (m n : ℤ) (P : A) :
    P ∈ (linePencil ψ m n).ker ↔ m • P = n • ψ P := by
  rw [AddMonoidHom.mem_ker, linePencil_apply, sub_eq_zero]

end Pencil

section Frobenius

variable {R : Type*} {S : Type*} {k : Type*} [CommRing R] [CommRing S] [Field k] [DecidableEq k]
  [Algebra R S] [Algebra R k] [Algebra S k] [IsScalarTower R S k]
  (W : WeierstrassCurve R) (σ : k ≃ₐ[S] k)

abbrev frobEnd : (W⁄k).Point →+ (W⁄k).Point :=
  DistribSMul.toAddMonoidHom (W⁄k).Point σ

lemma frobEnd_apply (P : (W⁄k).Point) : frobEnd W σ P = σ • P :=
  rfl

abbrev frobPencilEnd (p : ℕ) (m n : ℤ) :
    Module.End (ZMod p) (Submodule.torsionBy ℤ (W⁄k).Point p) :=
  ((m : ZMod p) • (1 : Module.End (ZMod p) (Submodule.torsionBy ℤ (W⁄k).Point p))) -
    (n : ZMod p) • galoisRepModuleEnd S W p σ

def FrobCharEqOnPoints (a : ℤ) (q : ℕ) : Prop :=
  ∀ P : (W⁄k).Point, σ • (σ • P) - a • (σ • P) + (q : ℤ) • P = 0

end Frobenius

end FrobeniusEndo

end

Statements phrased using this module (21)