Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_FibrePoly.lean

definition module

Fibre polynomials of a bivariate modular polynomial

Throughout, k is a field, \ell a prime and k has characteristic \ell; bivariate polynomials are taken in the iterated form \mathbb{Z}[X][Y], with X the inner and Y the outer variable.

For \Phi \in \mathbb{Z}[X][Y] and a \in k, fibrePoly \Phi\,a is the univariate polynomial \Phi(a, Y) \in k[Y] obtained by applying to each coefficient of \Phi the ring homomorphism \mathbb{Z}[X] \to k that casts integer coefficients into k and sends X \mapsto a. Thus the inner variable is specialised at a and the outer variable is kept; the roots of fibrePoly \Phi\,a, with multiplicity, are the fibre over a of the correspondence cut out by \Phi.

Two identities record that this specialisation factors through reduction modulo \ell. First, eval₂RingHom_intCast_eq_comp states that the homomorphism \mathbb{Z}[X] \to k just described equals coefficientwise reduction \mathbb{Z}[X] \to \mathbb{F}_\ell[X] followed by evaluation at a along the canonical map \mathbb{F}_\ell \to k (ZMod.castHom). Consequently, fibrePoly_eq_map_reduceModBivar gives \Phi(a,Y) = \bar{\Phi}(a,Y), where \bar{\Phi} = reduceModBivar \ell\,\Phi is the coefficientwise reduction of \Phi to \mathbb{F}_\ell[X][Y]: the fibre polynomial only depends on \Phi \bmod \ell. This is what allows a congruence for \Phi modulo \ell, such as the Kronecker congruence \bar{\Phi} = (X^\ell - Y)(X - Y^\ell) encoded by KroneckerCongruence, to be used fibre by fibre.

Finally, C_sub_X_pow_eq_neg_pow assumes in addition that k is perfect of characteristic \ell and asserts, for a \in k, the identity a - Y^{\ell} = -\bigl(Y - a^{1/\ell}\bigr)^{\ell} in k[Y], where a^{1/\ell} is the image of a under the inverse of the Frobenius bijection. It exhibits the second Kronecker factor, specialised at a, as \ell times the point a^{1/\ell} up to sign.

Relation to Mathlib

Mathlib supplies the ingredients (Polynomial.map, Polynomial.eval₂RingHom, ZMod.castHom, the freshman's dream sub_pow_expChar, and frobeniusEquiv for perfect rings); the specialisation operator fibrePoly on bivariate integral polynomials is the project's own packaging.

Where it is used

These are the bridge between a congruence modulo \ell for a modular polynomial, in the shape of the Kronecker congruence \Phi \equiv (X^{\ell} - Y)(X - Y^{\ell}), and the geometry of the fibres of the associated correspondence over a field of characteristic \ell. They are used in the analysis of the special fibre at \ell, where the two Kronecker factors give the Frobenius and Verschiebung parts of the Hecke correspondence, towards the Eichler–Shimura congruence relation that governs the Galois representations attached to modular forms.

References

  1. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Publications of the Mathematical Society of Japan 11, Princeton University Press, 1971, Chapter 5
  2. S. Lang, Elliptic Functions, 2nd edition, Graduate Texts in Mathematics 112, Springer, 1987, Chapter 5

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_KroneckerTransport

noncomputable section

open Polynomial

namespace ModularCurve

section FibrePoly

variable {k : Type*} [Field k]

def fibrePoly (Φ : Polynomial (Polynomial ℤ)) (a : k) : Polynomial k :=
  Φ.map (Polynomial.eval₂RingHom (Int.castRingHom k) a)

variable {ℓ : ℕ} [Fact ℓ.Prime] [CharP k ℓ]

theorem eval₂RingHom_intCast_eq_comp (a : k) :
    Polynomial.eval₂RingHom (Int.castRingHom k) a =
      (Polynomial.eval₂RingHom (ZMod.castHom (dvd_refl ℓ) k) a).comp
        (Polynomial.mapRingHom (Int.castRingHom (ZMod ℓ))) := by
  refine Polynomial.ringHom_ext' (Subsingleton.elim _ _) ?_
  rw [Polynomial.coe_eval₂RingHom, Polynomial.eval₂_X, RingHom.comp_apply,
    Polynomial.coe_mapRingHom, Polynomial.map_X, Polynomial.coe_eval₂RingHom,
    Polynomial.eval₂_X]

theorem fibrePoly_eq_map_reduceModBivar (Φ : Polynomial (Polynomial ℤ)) (a : k) :
    fibrePoly Φ a =
      (reduceModBivar ℓ Φ).map
        (Polynomial.eval₂RingHom (ZMod.castHom (dvd_refl ℓ) k) a) := by
  rw [fibrePoly, eval₂RingHom_intCast_eq_comp (ℓ := ℓ),
    show reduceModBivar ℓ Φ
      = Φ.map (Polynomial.mapRingHom (Int.castRingHom (ZMod ℓ))) from rfl,
    Polynomial.map_map]

end FibrePoly

section Factorization

variable {k : Type*} [Field k] {ℓ : ℕ} [Fact ℓ.Prime] [CharP k ℓ] [PerfectRing k ℓ]

theorem C_sub_X_pow_eq_neg_pow (a : k) :
    Polynomial.C a - Polynomial.X ^ ℓ =
      -((Polynomial.X - Polynomial.C ((frobeniusEquiv k ℓ).symm a)) ^ ℓ) := by
  have hpoly : (Polynomial.X - Polynomial.C ((frobeniusEquiv k ℓ).symm a)) ^ ℓ =
      Polynomial.X ^ ℓ - Polynomial.C ((frobeniusEquiv k ℓ).symm a) ^ ℓ :=
    sub_pow_expChar _ _
  rw [hpoly, ← Polynomial.C_pow, frobeniusEquiv_symm_pow_p, neg_sub]

end Factorization

end ModularCurve

Statements phrased using this module (19)