Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_CupPairing.lean

definition module

Rational cup-product pairing on additive characters of

Throughout, \Gamma is a subgroup of \mathrm{SL}_2(\mathbb Z) and \varphi,\psi are additive homomorphisms from \Gamma (written additively) to \mathbb Q. Three things are defined. First, IsPrimitive, a predicate on a function h\colon G\to R attached to two additive characters \varphi,\psi\colon G\to R of an arbitrary group G with values in a commutative ring R: it asserts h(gg')=h(g)+h(g')-\omega(g,g') for all g,g', where \omega(g,g')=\varphi(g)\psi(g')-\psi(g)\varphi(g') is the antisymmetrised cup-product cocycle of ModularCurve.PDPairing.omega. Thus h is a primitive, i.e. a set-theoretic splitting datum for the central extension cut out by \omega. Second, mult, the rational number equal to 1 if -1\in\Gamma and to 2 otherwise; mult_ne_zero records that it is nonzero. Third, pair, a rational number \langle\varphi,\psi\rangle defined by a double case distinction: if \Gamma has finite index and a primitive h for \varphi,\psi exists, it is \mathrm{cuspSum}_\Gamma(h)/(2\,\mathrm{mult}\,\Gamma) for a primitive h selected by the axiom of choice from the existence hypothesis, and it is 0 in either of the two remaining cases. Here \mathrm{cuspSum}_\Gamma(h)=\sum_q h(\pi_q) is the sum of ModularCurve.PDPairing.cuspSum, indexed by the orbits q of the cyclic group generated by T=\begin{pmatrix}1&1\\0&1\end{pmatrix} acting on \mathrm{SL}_2(\mathbb Z)/\Gamma, with \pi_q=x_q^{-1}T^{w_q}x_q\in\Gamma the generator of cuspGen, w_q the minimal period of the orbit. The accompanying lemmas unwind the branches: pair_eq_dif gives the stated formula when \Gamma has finite index and a primitive exists, while pair_eq_zero_of_not_exists and pair_eq_zero_of_not_finiteIndex give the value 0 in the two degenerate cases. No properties of the pairing itself (bilinearity, antisymmetry, independence of the chosen primitive) are asserted here.

Relation to Mathlib

Mathlib has no cup-product or intersection pairing on the cohomology of modular curves, nor the notion of a primitive of the antisymmetrised cocycle \omega; both are the project's own, built on Mathlib's congruence subgroups, group transfer, and Nielsen–Schreier freeness.

Where it is used

The pairing defined here is the rational-valued cup-product pairing on additive characters of a finite-index subgroup of \mathrm{SL}_2(\mathbb Z), the group-theoretic incarnation of the intersection pairing on the homology of the compact modular curve; it feeds the treatment of parabolic homomorphisms and of the Hecke action on them used in the modular-curve input to the argument.

References

  1. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Publications of the Mathematical Society of Japan 11, Princeton University Press, 1971
  2. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_PDPairing

set_option autoImplicit false

namespace ModularCurve.CupPairing

open scoped MatrixGroups

def IsPrimitive {G : Type*} [Group G] {R : Type*} [CommRing R] (φ ψ : Additive G →+ R)
    (h : G → R) : Prop :=
  ∀ g g' : G, h (g * g') = h g + h g' - ModularCurve.PDPairing.omega φ ψ g g'

noncomputable def mult (Γ : Subgroup SL(2, ℤ)) : ℚ := by
  classical
  exact if (-1 : SL(2, ℤ)) ∈ Γ then 1 else 2

noncomputable def pair (Γ : Subgroup SL(2, ℤ)) (φ ψ : Additive Γ →+ ℚ) : ℚ := by
  classical
  exact if hΓ : Γ.FiniteIndex then
      if hp : ∃ h : Γ → ℚ, IsPrimitive φ ψ h then
        (@ModularCurve.PDPairing.cuspSum Γ hΓ ℚ _ (Classical.choose hp)) / (2 * mult Γ)
      else 0
    else 0

theorem pair_eq_dif (Γ : Subgroup SL(2, ℤ)) [hΓ : Γ.FiniteIndex] (φ ψ : Additive Γ →+ ℚ)
    (hp : ∃ h : Γ → ℚ, IsPrimitive φ ψ h) :
    pair Γ φ ψ = ModularCurve.PDPairing.cuspSum Γ (Classical.choose hp) / (2 * mult Γ) := by
  unfold pair
  rw [dif_pos hΓ, dif_pos hp]

theorem pair_eq_zero_of_not_exists (Γ : Subgroup SL(2, ℤ)) (φ ψ : Additive Γ →+ ℚ)
    (hp : ¬ ∃ h : Γ → ℚ, IsPrimitive φ ψ h) : pair Γ φ ψ = 0 := by
  unfold pair
  split_ifs <;> rfl

theorem pair_eq_zero_of_not_finiteIndex (Γ : Subgroup SL(2, ℤ)) (φ ψ : Additive Γ →+ ℚ)
    (hΓ : ¬ Γ.FiniteIndex) : pair Γ φ ψ = 0 := by
  unfold pair
  rw [dif_neg hΓ]

theorem mult_ne_zero (Γ : Subgroup SL(2, ℤ)) : mult Γ ≠ 0 := by
  unfold mult
  split_ifs <;> norm_num

end ModularCurve.CupPairing

Statements phrased using this module (7)