Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_AbelFibreSumOf.lean

definition module

Orbifold index and fibre-sum functional for a general level

For a subgroup \Gamma \le \mathrm{SL}_2(\mathbb{Z}) two objects are defined on the upper half plane \mathfrak{H}, at arbitrary level rather than only for \Gamma_0(N).

First, ModularCurve.orbifoldIndexOf Γ τ is the natural number \#\mathrm{Stab}(\tau) / 2, where the stabiliser is taken for the action of the subgroup \Gamma \sqcup \langle -1 \rangle of \mathrm{SL}_2(\mathbb{Z}) generated by \Gamma together with the powers of -1, its cardinality is Nat.card (so 0 when the stabiliser is infinite), and the division is truncated division of naturals. Passing to the group generated by \Gamma and -1 makes the quantity the order of the image of the stabiliser in \mathrm{PSL}_2(\mathbb{Z}) whether or not -1 \in \Gamma; no hypothesis on -1 is imposed.

Second, for a function F : \mathfrak{H} \to \mathbb{C} and t \in \mathbb{C}, ModularCurve.abelFibreSumOf Γ F t is an element of the \mathbb{C}-linear dual of the space CuspForm Γ 2 of weight-two cusp forms for \Gamma, namely the finitely supported sum (∑ᶠ, which is 0 when the family has infinite support) over the orbit space \Gamma \backslash \mathfrak{H} of \frac{m_t(\xi^{\mathrm{out}})}{e_{\xi^{\mathrm{out}}}} \cdot P(\xi^{\mathrm{out}}), where \xi^{\mathrm{out}} is the chosen representative Quotient.out of the orbit \xi, e_\tau is orbifoldIndexOf Γ τ, the coefficient is formed by casting both naturals into \mathbb{C} and dividing (so a vanishing index yields coefficient 0), and m_t(\tau) is the imported ModularCurve.valueMultiplicity F t τ: the meromorphic order at \tau of z \mapsto F(z) - t, read through ofComplex, with \top sent to 0 and negative orders truncated to 0. The functional P(\tau) = periodAlongOf Γ UpperHalfPlane.I τ sends f to \int_0^1 f(\sigma(s))\,(\tau - i)\,ds along the straight segment \sigma from i to \tau. Two further lemmas record these two definitions as equations.

Relation to Mathlib

Mathlib supplies the upper half plane with its \mathrm{SL}_2(\mathbb{Z})-action, CuspForm, meromorphicOrderAt and the finite sum ∑ᶠ; the orbifold index and the fibre-sum functional are the project's own notions, and they are the general-\Gamma counterparts of ModularCurve.orbifoldIndex and ModularCurve.abelFibreSum, which are stated for CongruenceSubgroup.Gamma0 N.

Where it is used

The fibre sum is the Abel–Jacobi image, with base point i, of the divisor of a \Gamma-invariant function above a value t, expressed as a functional on weight-two cusp forms; it feeds the period-lattice integrality statements used in the analytic input to the Eichler–Shimura theory of the modular Jacobian.

References

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

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_PeriodOf
import Definitions.Def_ModularCurve_AbelFibreSum

set_option autoImplicit false

noncomputable section

open UpperHalfPlane
open scoped MatrixGroups

namespace ModularCurve

variable (Γ : Subgroup SL(2, ℤ))

def orbifoldIndexOf (τ : ℍ) : ℕ :=
  Nat.card (MulAction.stabilizer
    (Γ ⊔ Subgroup.zpowers (-1 : SL(2, ℤ)) : Subgroup SL(2, ℤ)) τ) / 2

def abelFibreSumOf (F : ℍ → ℂ) (t : ℂ) : Module.Dual ℂ (CuspForm Γ 2) :=
  ∑ᶠ ξ : Quotient (MulAction.orbitRel Γ ℍ),
    ((valueMultiplicity F t ξ.out : ℂ) / (orbifoldIndexOf Γ ξ.out : ℂ)) •
      periodAlongOf Γ UpperHalfPlane.I ξ.out

theorem orbifoldIndexOf_def (τ : ℍ) :
    orbifoldIndexOf Γ τ =
      Nat.card (MulAction.stabilizer
        (Γ ⊔ Subgroup.zpowers (-1 : SL(2, ℤ)) : Subgroup SL(2, ℤ)) τ) / 2 :=
  rfl

theorem abelFibreSumOf_def (F : ℍ → ℂ) (t : ℂ) :
    abelFibreSumOf Γ F t =
      ∑ᶠ ξ : Quotient (MulAction.orbitRel Γ ℍ),
        ((valueMultiplicity F t ξ.out : ℂ) / (orbifoldIndexOf Γ ξ.out : ℂ)) •
          periodAlongOf Γ UpperHalfPlane.I ξ.out :=
  rfl

end ModularCurve

end

Statements phrased using this module (2)