`Definitions/Def_ModularCurve_CharLSpecialFibrePic0ForallMBridge.lean`

definition module

Eichler–Shimura special-fibre relation on Pic⁰, level by level

Four statements turn the geometric identities satisfied by Frobenius on the degree-zero Picard group of the characteristic-\ell modular function field into the project's abstract relation predicate, first at a single level and then uniformly in the level. A private auxiliary works purely abstractly: for an additive commutative group J' carrying a HeckeAlg-module structure, a prime \ell, and additive endomorphisms F,V,T of J' with T = F + V pointwise, V(F y) = \ell y for all y, and the generator heckeGen ⟨ℓ, hℓ⟩ acting as T, it yields SpecialFibreRelation J' ℓ hℓ F, the project predicate recording the quadratic relation satisfied by F at \ell relative to the action of that generator. specialFibreRelation_pic0_level_of_match specialises this: for a field K of characteristic \ell, a level N \ge 1, Kronecker data data : ModularPolynomialData ℓ with hKr : KroneckerCongruence ℓ data, the hypothesis that every element of K is an \ell-th power, and the hypothesis that every place of modularFunctionFieldC K N over K (the subfield of K((q)) generated by the j-series and its level-N transform) has residue degree 1, any HeckeAlg-module structure on Pic0 K (modularFunctionFieldC K N) whose generator at \ell acts as heckeFibreGeomLevelPic0 makes frobeniusPushforwardGeomLevelPic0 satisfy the relation; the inputs cited are the decomposition of the Hecke fibre operator as Frobenius pushforward plus pullback and the composite pullback-after-pushforward being multiplication by \ell. A variant replaces the perfectness and degree hypotheses by K algebraically closed together with IsCurveOver K (modularFunctionFieldC K N) (principal divisors, finite residue extensions, and Kähler differentials free of rank one), and packages the matching hypothesis as SpecialFibreHeckeModuleMatch. Finally, under a family hypothesis IsCurveOverModularFunctionFieldCFamily K supplying the curve structure at every level, four statements assert at all levels N \ge 1 and all x: the relation F(F x) - T(F x) + (\ell : \mathbb{Z}) \cdot x = 0, the identity T = F + V, the identity V(F x) = (\ell : \mathbb{Z}) \cdot x, and, given per-level module structures and matching hypotheses, SpecialFibreRelation at every level.

Relation to Mathlib

Mathlib has no Hecke algebra acting on degree-zero Picard groups of function fields and no Eichler–Shimura congruence; Place, Pic0, IsCurveOver and the Frobenius pushforward/pullback operators are the project's own notions, built on Mathlib's valuation subrings, divisors as finitely supported functions and Kähler differentials.

Where it is used

These statements are the interface between the geometric Eichler–Shimura congruence on the Jacobian of the characteristic-\ell modular curve and the abstract relation predicate consumed downstream, where the relation is used to compare Frobenius eigenvalues with Hecke eigenvalues in the modularity and level-lowering arguments of the Fermat route.

References

G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Publications of the Mathematical Society of Japan 11, Princeton University Press, 1971, Chapter 7
J. Igusa, Kroneckerian model of fields of elliptic modular functions, American Journal of Mathematics 81 (1959), 561–577

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

127 lines
7 declarations
used in the statements of 0 theorems and imported by 0 proofs
imports 1 definition modules

Source file: Definitions/Def_ModularCurve_CharLSpecialFibrePic0ForallMBridge.lean

Imports

Def_ModularCurve_CharLFrobeniusGeomLevel

Imported by

Def_ModularCurve_CharLSpecialFibrePic0CommutingFamilyBridge

Declarations

theoremModularCurve.specialFibreRelation_of_decomp_of_verFrob_aux
theoremModularCurve.specialFibreRelation_pic0_level_of_match
theoremModularCurve.specialFibreRelation_pic0_level_of_isCurveOver_of_match
theoremModularCurve.forall_eichlerShimura_special_fibre_pic0_of_curveOverFamily
theoremModularCurve.forall_heckeFibreGeomLevelPic0_eq_add_of_curveOverFamily
theoremModularCurve.forall_frobeniusPullbackPushforwardGeomLevelPic0_of_curveOverFamily
theoremModularCurve.forall_specialFibreRelation_pic0_of_curveOverFamily_of_matchFamily

Source

import Mathlib
import Definitions.Def_ModularCurve_CharLFrobeniusGeomLevel

set_option autoImplicit false
set_option synthInstance.maxHeartbeats 400000
set_option maxHeartbeats 800000

noncomputable section

open AlgebraicCurve

namespace ModularCurve

section AbstractDictionary

variable {J' : Type*} [AddCommGroup J'] [Module HeckeAlg J']
variable {ℓ : ℕ}

private theorem specialFibreRelation_of_decomp_of_verFrob_aux (hℓ : ℓ.Prime)
    {F V T : J' →+ J'}
    (hdecomp : ∀ y : J', T y = F y + V y)
    (hVF : ∀ y : J', V (F y) = ℓ • y)
    (hmatch : ∀ y : J', heckeGen ⟨ℓ, hℓ⟩ • y = T y) :
    SpecialFibreRelation J' ℓ hℓ F := by
  intro y
  rw [hmatch, hdecomp, hVF]; abel

end AbstractDictionary

section Bridge

variable (K : Type*) [Field K] (N : ℕ) [NeZero N]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP K ℓ]
variable (data : ModularPolynomialData ℓ) (hKr : KroneckerCongruence ℓ data)
variable (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c)
variable (hdeg1 : ∀ w : Place K (modularFunctionFieldC K N), w.deg = 1)

theorem specialFibreRelation_pic0_level_of_match
    (inst : Module HeckeAlg (Pic0 K (modularFunctionFieldC K N)))
    (hmatch : ∀ x, (letI := inst; heckeGen ⟨ℓ, hℓ.out⟩ • x)
        = heckeFibreGeomLevelPic0 K N data hKr hperf hdeg1 x) :
    letI := inst
    SpecialFibreRelation (Pic0 K (modularFunctionFieldC K N)) ℓ hℓ.out
      (frobeniusPushforwardGeomLevelPic0 K N data hKr hperf hdeg1) := by
  letI := inst
  refine specialFibreRelation_of_decomp_of_verFrob_aux hℓ.out
    (V := frobeniusPullbackGeomLevelPic0 K N data hKr hperf hdeg1)
    (T := heckeFibreGeomLevelPic0 K N data hKr hperf hdeg1)
    (heckeFibreGeomLevelPic0_eq_add K N data hKr hperf hdeg1)
    (fun y => ?_) hmatch
  have h := frobeniusPullbackGeomLevelPic0_frobeniusPushforwardGeomLevelPic0
    K N data hKr hperf hdeg1 y
  rw [h, natCast_zsmul]

variable [IsAlgClosed K] [IsCurveOver K (modularFunctionFieldC K N)]

theorem specialFibreRelation_pic0_level_of_isCurveOver_of_match
    (inst : Module HeckeAlg (Pic0 K (modularFunctionFieldC K N)))
    (hmatch : SpecialFibreHeckeModuleMatch K N data hKr inst) :
    letI := inst
    SpecialFibreRelation (Pic0 K (modularFunctionFieldC K N)) ℓ hℓ.out
      (frobeniusPushforwardGeomLevelPic0OfIsCurveOver K N data hKr) :=
  specialFibreRelation_pic0_level_of_match K N data hKr (perfect_of_isAlgClosed K)
    (deg_eq_one_modularFunctionFieldC K N) inst hmatch

end Bridge

section ForallM

variable (K : Type*) [Field K] [IsAlgClosed K]
variable {ℓ : ℕ} [Fact ℓ.Prime] [CharP K ℓ]
variable (data : ModularPolynomialData ℓ) (hKr : KroneckerCongruence ℓ data)
variable (hfam : IsCurveOverModularFunctionFieldCFamily K)

theorem forall_eichlerShimura_special_fibre_pic0_of_curveOverFamily :
    ∀ (N : ℕ) [NeZero N],
      letI := hfam N
      ∀ x : Pic0 K (modularFunctionFieldC K N),
        frobeniusPushforwardGeomLevelPic0OfIsCurveOver K N data hKr
            (frobeniusPushforwardGeomLevelPic0OfIsCurveOver K N data hKr x)
          - heckeFibreGeomLevelPic0OfIsCurveOver K N data hKr
              (frobeniusPushforwardGeomLevelPic0OfIsCurveOver K N data hKr x)
          + (ℓ : ℤ) • x = 0 := by
  intro N _
  letI := hfam N
  exact eichlerShimura_special_fibre_pic0_level_of_isCurveOver K N data hKr

theorem forall_heckeFibreGeomLevelPic0_eq_add_of_curveOverFamily :
    ∀ (N : ℕ) [NeZero N],
      letI := hfam N
      ∀ x : Pic0 K (modularFunctionFieldC K N),
        heckeFibreGeomLevelPic0OfIsCurveOver K N data hKr x
          = frobeniusPushforwardGeomLevelPic0OfIsCurveOver K N data hKr x
            + frobeniusPullbackGeomLevelPic0OfIsCurveOver K N data hKr x := by
  intro N _
  letI := hfam N
  exact heckeFibreGeomLevelPic0OfIsCurveOver_eq_add K N data hKr

theorem forall_frobeniusPullbackPushforwardGeomLevelPic0_of_curveOverFamily :
    ∀ (N : ℕ) [NeZero N],
      letI := hfam N
      ∀ x : Pic0 K (modularFunctionFieldC K N),
        frobeniusPullbackGeomLevelPic0OfIsCurveOver K N data hKr
            (frobeniusPushforwardGeomLevelPic0OfIsCurveOver K N data hKr x)
          = (ℓ : ℤ) • x := by
  intro N _
  letI := hfam N
  exact frobeniusPullbackPushforwardGeomLevelPic0OfIsCurveOver K N data hKr

theorem forall_specialFibreRelation_pic0_of_curveOverFamily_of_matchFamily
    (instfam : ∀ (N : ℕ) [NeZero N],
      letI := hfam N; Module HeckeAlg (Pic0 K (modularFunctionFieldC K N)))
    (hmatchfam : ∀ (N : ℕ) [NeZero N],
      letI := hfam N; SpecialFibreHeckeModuleMatch K N data hKr (instfam N)) :
    ∀ (N : ℕ) [NeZero N],
      letI := hfam N; letI := instfam N
      SpecialFibreRelation (Pic0 K (modularFunctionFieldC K N)) ℓ (Fact.out)
        (frobeniusPushforwardGeomLevelPic0OfIsCurveOver K N data hKr) := by
  intro N _
  letI := hfam N
  exact specialFibreRelation_pic0_level_of_isCurveOver_of_match K N data hKr
    (instfam N) (hmatchfam N)

end ForallM

end ModularCurve

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).