Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_ShimuraKernel.lean

definition module

Shimura covering pullback and the Shimura kernel in

The first part of the module transports the Picard pullback of degree-zero divisor classes along an algebra homomorphism of function fields. For fields K \subseteq F, K \subseteq F' with F' having principal divisors, an K-algebra map \varphi : F \to F' whose underlying ring homomorphism is integral, and a witness hFI of FundamentalIdentityAlong (for every place v of F, \sum_{w \mid v} e(w)\deg(w) = [F':F]\deg(v), computed for the F-algebra structure on F' induced by \varphi), pullbackAlongDegZeroHom is the restriction of the divisor pullback Divisor.pullbackAlong to divisors of degree zero — legitimate because the degree of a pullback is [F':F] times the degree — and pullbackAlongHom is the induced additive map \mathrm{Pic}^0(K,F) \to \mathrm{Pic}^0(K,F'), obtained by passing to the quotient by principal divisors, pullbacks of principal divisors being principal.

The second part specialises this to the Shimura covering of X_0(p). Here shimuraFunctionFieldBar p is the base change to \overline{\mathbb{Q}}, inside Laurent series over \overline{\mathbb{Q}}, of shimuraFunctionField p, the subfield of \mathbb{Q}((q)) generated by the expansions j(q^d) for d \mid p together with the series shimuraGenSeries p v, v \in (\mathbb{Z}/p)^\times; it contains the corresponding base change modularFunctionFieldBar p of the field generated by the j(q^d) alone, and shimuraInclusion p is the resulting inclusion of \overline{\mathbb{Q}}-algebras. The structure ShimuraCoveringInputs p is a proposition packaging three hypotheses about this inclusion: that it is integral, that the larger field has principal divisors, and that the fundamental identity holds along it. Given such an input I, shimuraPicardPullback I is the pullback map from JZero p (the degree-zero Picard group of modularFunctionFieldBar p) to the degree-zero Picard group of shimuraFunctionFieldBar p, and shimuraKernel I is its kernel, an additive subgroup of JZero p.

Relation to Mathlib

Mathlib has no divisor theory or degree-zero Picard group for function fields of curves; the places, divisors, pullback/pushforward maps and the FundamentalIdentity condition used here belong to the project's own algebraic-curve layer, built over Mathlib's valuation subrings and Laurent series. The …Along maps of this module are the versions of that layer's pullback transported along an algebra homomorphism rather than along an Algebra instance.

Where it is used

shimuraKernel is the concrete realisation, as a kernel of a Picard pullback, of Mazur's Shimura subgroup of J_0(p); its properties (multiplicative type, order the numerator of (p-1)/12, Eisenstein behaviour under Hecke operators) are what the project's predicate IsShimuraSubgroup abstracts, and they feed the Eisenstein-ideal input to level lowering for J_0(p).

References

  1. B. Mazur, Modular curves and the Eisenstein ideal, Publications Mathématiques de l'IHÉS 47 (1977), 33–186, Chapter II, §11
  2. S. Ling and J. Oesterlé, The Shimura subgroup of J_0(N), Astérisque 196–197 (1991), 171–203

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

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_ShimuraSubgroup
import Definitions.Def_ModularCurve_ShimuraGenerator
import Definitions.Def_AlgebraicCurve_Correspondence

set_option autoImplicit false

noncomputable section

namespace AlgebraicCurve

namespace Pic0

open Divisor

variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable [HasPrincipalDivisors K F']
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
variable (hFI : FundamentalIdentityAlong K φ hφ)

def pullbackAlongDegZeroHom :
    Divisor.degZero (K := K) (F := F) →+ Divisor.degZero (K := K) (F := F') :=
  ((Divisor.pullbackAlong φ hφ).domRestrict (Divisor.degZero (K := K) (F := F))).codRestrict _
    (fun D => Divisor.pullbackAlong_mem_degZero φ hφ hFI D.2)

@[simp]
theorem coe_pullbackAlongDegZeroHom (D : Divisor.degZero (K := K) (F := F)) :
    (pullbackAlongDegZeroHom φ hφ hFI D : Divisor K F') =
      Divisor.pullbackAlong φ hφ (D : Divisor K F) :=
  rfl

def pullbackAlongHom : Pic0 K F →+ Pic0 K F' :=
  QuotientAddGroup.map _ _ (pullbackAlongDegZeroHom φ hφ hFI) (by
    rintro ⟨D, hD0⟩ hD
    simp only [AddSubgroup.mem_addSubgroupOf] at hD ⊢
    exact Divisor.isPrincipal_pullbackAlong φ hφ hD)

theorem pullbackAlongHom_mk (D : Divisor.degZero (K := K) (F := F)) :
    pullbackAlongHom φ hφ hFI (mk D) = mk (pullbackAlongDegZeroHom φ hφ hFI D) :=
  rfl

end Pic0

end AlgebraicCurve

namespace ModularCurve

open AlgebraicCurve IntermediateField

variable (p : ℕ)

abbrev shimuraFunctionFieldBar :
    IntermediateField (AlgebraicClosure ℚ) (LaurentSeries (AlgebraicClosure ℚ)) :=
  laurentBaseChange (AlgebraicClosure ℚ) (shimuraFunctionField p)

theorem modularFunctionFieldBar_le_shimuraFunctionFieldBar :
    modularFunctionFieldBar p ≤ shimuraFunctionFieldBar p := by
  show laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull p)
    ≤ laurentBaseChange (AlgebraicClosure ℚ) (shimuraFunctionField p)
  unfold laurentBaseChange
  exact IntermediateField.adjoin.mono _ _ _
    (Set.image_mono (modularFunctionFieldFull_le_shimuraFunctionField p))

def shimuraInclusion :
    (modularFunctionFieldBar p) →ₐ[AlgebraicClosure ℚ] (shimuraFunctionFieldBar p) :=
  IntermediateField.inclusion (modularFunctionFieldBar_le_shimuraFunctionFieldBar p)

structure ShimuraCoveringInputs : Prop where

  hint : (shimuraInclusion p).toRingHom.IsIntegral

  hpd : HasPrincipalDivisors (AlgebraicClosure ℚ) (shimuraFunctionFieldBar p)

  hFI : haveI := hpd; FundamentalIdentityAlong (AlgebraicClosure ℚ) (shimuraInclusion p) hint

variable {p} in

def shimuraPicardPullback (I : ShimuraCoveringInputs p) :
    JZero p →+ Pic0 (AlgebraicClosure ℚ) (shimuraFunctionFieldBar p) :=
  haveI := I.hpd
  Pic0.pullbackAlongHom (shimuraInclusion p) I.hint I.hFI

variable {p} in

def shimuraKernel (I : ShimuraCoveringInputs p) : AddSubgroup (JZero p) :=
  (shimuraPicardPullback I).ker

end ModularCurve

end

Statements phrased using this module (17)