Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_JZeroSemistableSpecialization.lean

definition module

Semistable specialization data for at

Three auxiliary notions are introduced first. For q\in\mathbb N and an element x of an additive monoid, PrimeToTorsion q x asserts that n\cdot x=0 for some n>0 with q\nmid n, i.e. x is torsion of order prime to q; the accompanying lemmas record that 0 satisfies it when q\neq 1, that it is preserved by addition (for q prime), by negation, and by additive monoid homomorphisms. For a subgroup I of a group G acting distributively on an abelian group M, smulInvariants I M is the additive subgroup \{x : \sigma\cdot x=x \text{ for all }\sigma\in I\}, and inertiaInvariants A M specialises this to I= the inertia subgroup of a valuation subring A of \overline{\mathbb Q} over \mathbb Q acting on JZero\,M=\mathrm{Pic}^0 of the level-M modular function field over \overline{\mathbb Q}.

The structure JZeroSemistableSpecialization, formed for a valuation subring A of \overline{\mathbb Q}, naturals N (nonzero) and q with q prime, and Hecke-module structures on the relevant groups, bundles as fields the data and properties of a semistable specialization. Writing \kappa for the residue field of A and F= modularFunctionFieldC \kappa\,N (the subfield of \kappa((t)) generated by the j- and j_N-expansions), it carries: a finite set nodes of pairs of places of F/\kappa, each place having residue field generated by \kappa; a \kappa-semilinear automorphism frob of F whose base automorphism is a\mapsto a^q, which permutes nodes by an involution; a width function nodes → ℕ; a homomorphism comp from the inertia invariants of JZero(Nq) to the component group of the width-weighted Gram pairing on the degree-zero character lattice of nodes, on which T_\ell acts by \ell+1 for \ell\nmid Nq and whose kernel is stable under the Hecke algebra and under any Frobenius at q; a homomorphism sp to the glued \mathrm{Pic}^0 of (F,\text{nodes}), which on the kernel of comp is T_\ell-equivariant after projection to \mathrm{Pic}^0\times\mathrm{Pic}^0, intertwines Frobenius at q with the glued map glueMap, sends T_q on the subgroup of node-unit classes to the permutation action induced by nodePerm, and is injective on prime-to-q torsion in the kernel of comp; the assertion that Hecke eigen-torsion for a maximal ideal \mathfrak m with q invertible in HeckeAlg/\mathfrak m is killed by some prime p\neq q; and a Hecke-equivariant specialization spN of JZero\,N into \mathrm{Pic}^0(F) that is injective on prime-to-q torsion and hits every prime-to-q torsion class by a prime-to-q torsion element. The structure is a carrier of hypotheses: it asserts nothing about existence of such data.

Relation to Mathlib

Mathlib has no notion of glued \mathrm{Pic}^0, of the component group of a weighted dual graph, or of specialization data for modular Jacobians; these rest on the project's own GluedPic0, componentGroup and JZero. PrimeToTorsion is a bespoke predicate for torsion of order prime to a fixed q, and smulInvariants packages the fixed points of a DistribMulAction of a subgroup as an AddSubgroup.

Where it is used

These definitions supply the language for the level-lowering step at the auxiliary prime q: the special fibre of X_0(Nq) at q is described as two copies of the level-N curve glued along pairs of nodes, and a mod-p Hecke eigensystem occurring in J_0(Nq) with trivial component-group contribution is transferred to J_0(N) through sp and spN.

References

  1. K. A. Ribet, On modular representations of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) arising from modular forms, Inventiones Mathematicae 100 (1990), 431–476
  2. P. Deligne and M. Rapoport, Les schémas de modules de courbes elliptiques, in: Modular Functions of One Variable II, Lecture Notes in Mathematics 349, Springer, 1973, 143–316
  3. S. Bosch, W. Lütkebohmert and M. Raynaud, Néron Models, Ergebnisse der Mathematik und ihrer Grenzgebiete 21, Springer, 1990, §9.6

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

Imports

Imported by

Declarations

Source

import Definitions.Def_AlgebraicCurve_GluedPic0
import Definitions.Def_AlgebraicCurve_GluedPic0Functoriality
import Definitions.Def_ModularCurve_ArithmeticGalois
import Definitions.Def_ModularCurve_JqCoeff
import Definitions.Def_HeckeGalois_EichlerShimura
import Definitions.Def_ModularCurve_ComponentGroup

noncomputable section

namespace ModularCurve

open AlgebraicCurve IsLocalRing

local notation "Qbar" => AlgebraicClosure ℚ

section Generic

def PrimeToTorsion (q : ℕ) {M : Type*} [AddMonoid M] (x : M) : Prop :=
  ∃ n : ℕ, 0 < n ∧ ¬ q ∣ n ∧ n • x = 0

namespace PrimeToTorsion

variable {q : ℕ} {M M' : Type*}

theorem zero [AddMonoid M] (hq : q ≠ 1) : PrimeToTorsion q (0 : M) :=
  ⟨1, Nat.one_pos, fun h => hq (Nat.dvd_one.mp h), nsmul_zero _⟩

theorem add [AddCommMonoid M] (hq : q.Prime) {x y : M} (hx : PrimeToTorsion q x)
    (hy : PrimeToTorsion q y) : PrimeToTorsion q (x + y) := by
  obtain ⟨n, hn, hqn, hnx⟩ := hx
  obtain ⟨m, hm, hqm, hmy⟩ := hy
  refine ⟨n * m, Nat.mul_pos hn hm, fun h => (hq.dvd_mul.mp h).elim hqn hqm, ?_⟩
  rw [nsmul_add, mul_nsmul, hnx, nsmul_zero, zero_add, mul_comm n m, mul_nsmul, hmy, nsmul_zero]

theorem neg [AddCommGroup M] {x : M} (hx : PrimeToTorsion q x) : PrimeToTorsion q (-x) := by
  obtain ⟨n, hn, hqn, hnx⟩ := hx
  exact ⟨n, hn, hqn, by rw [neg_nsmul, hnx, neg_zero]⟩

theorem map [AddMonoid M] [AddMonoid M'] {F : Type*} [FunLike F M M'] [AddMonoidHomClass F M M']
    (f : F) {x : M} (hx : PrimeToTorsion q x) : PrimeToTorsion q (f x) := by
  obtain ⟨n, hn, hqn, hnx⟩ := hx
  exact ⟨n, hn, hqn, by rw [← map_nsmul, hnx, map_zero]⟩

end PrimeToTorsion

def smulInvariants {G : Type*} [Group G] (I : Subgroup G) (M : Type*) [AddCommGroup M]
    [DistribMulAction G M] : AddSubgroup M where
  carrier := {x | ∀ σ ∈ I, σ • x = x}
  zero_mem' := fun σ _ => smul_zero σ
  add_mem' := fun {x y} hx hy σ hσ => by rw [smul_add, hx σ hσ, hy σ hσ]
  neg_mem' := fun {x} hx σ hσ => by rw [smul_neg, hx σ hσ]

theorem mem_smulInvariants {G : Type*} [Group G] {I : Subgroup G} {M : Type*} [AddCommGroup M]
    [DistribMulAction G M] {x : M} : x ∈ smulInvariants I M ↔ ∀ σ ∈ I, σ • x = x :=
  Iff.rfl

end Generic

section Inertia

variable (A : ValuationSubring Qbar) (M : ℕ)

def inertiaInvariants : AddSubgroup (JZero M) :=
  smulInvariants (A.inertiaSubgroupIn ℚ) (JZero M)

variable {A M}

theorem mem_inertiaInvariants {x : JZero M} :
    x ∈ inertiaInvariants A M ↔ ∀ σ ∈ A.inertiaSubgroupIn ℚ, σ • x = x :=
  Iff.rfl

end Inertia

section Semistable

variable (A : ValuationSubring Qbar) (N q : ℕ) (hq : q.Prime) [NeZero N]

noncomputable local instance instDecidableEqResidueFieldSemistable :
    DecidableEq (ResidueField A) :=
  Classical.decEq _

set_option synthInstance.maxHeartbeats 80000 in

noncomputable local instance instAlgebraResidueFieldModularFunctionFieldCSemistable :
    Algebra (ResidueField A) (modularFunctionFieldC (ResidueField A) N) :=
  inferInstance

variable [Module HeckeAlg (JZero (N * q))] [Module HeckeAlg (JZero N)]
  [Module HeckeAlg (Pic0 (ResidueField A) (modularFunctionFieldC (ResidueField A) N))]

set_option synthInstance.maxHeartbeats 400000 in
set_option maxHeartbeats 4000000 in

structure JZeroSemistableSpecialization where

  nodes : Finset (Place (ResidueField A) (modularFunctionFieldC (ResidueField A) N) ×
    Place (ResidueField A) (modularFunctionFieldC (ResidueField A) N))

  nodes_rational : ∀ s ∈ nodes,
    Function.Surjective (algebraMap (ResidueField A) s.1.ResidueField) ∧
      Function.Surjective (algebraMap (ResidueField A) s.2.ResidueField)

  frob : SemilinearAut (ResidueField A) (modularFunctionFieldC (ResidueField A) N)

  frob_nodeStable : SemilinearAut.IsNodeStable nodes frob

  baseAut_frob : ∀ a : ResidueField A, SemilinearAut.baseAut frob a = a ^ q

  nodePerm_nodePerm : ∀ s : ↥nodes, SemilinearAut.nodePerm nodes frob frob_nodeStable
    (SemilinearAut.nodePerm nodes frob frob_nodeStable s) = s

  width : ↥nodes → ℕ

  comp : ↥(inertiaInvariants A (N * q)) →+ componentGroup width

  comp_heckeGen : ∀ ℓ : Nat.Primes, ¬ (ℓ : ℕ) ∣ N * q →
    ∀ (x : ↥(inertiaInvariants A (N * q)))
      (hx : heckeGen ℓ • (x : JZero (N * q)) ∈ inertiaInvariants A (N * q)),
      comp ⟨heckeGen ℓ • (x : JZero (N * q)), hx⟩ = (((ℓ : ℕ) : ℤ) + 1) • comp x

  comp_hecke_of_comp_eq_zero : ∀ (T : HeckeAlg) (x : ↥(inertiaInvariants A (N * q)))
      (hx : T • (x : JZero (N * q)) ∈ inertiaInvariants A (N * q)),
      comp x = 0 → comp ⟨T • (x : JZero (N * q)), hx⟩ = 0

  comp_frob_of_comp_eq_zero : ∀ φ : Qbar ≃ₐ[ℚ] Qbar, A.IsFrobeniusAt φ q →
    ∀ (x : ↥(inertiaInvariants A (N * q)))
      (hx : φ • (x : JZero (N * q)) ∈ inertiaInvariants A (N * q)),
      comp x = 0 → comp ⟨φ • (x : JZero (N * q)), hx⟩ = 0

  sp : ↥(inertiaInvariants A (N * q)) →+
    GluedPic0 (ResidueField A) (modularFunctionFieldC (ResidueField A) N) nodes

  toPic0Pair_sp_heckeGen : ∀ ℓ : Nat.Primes, ¬ (ℓ : ℕ) ∣ N * q →
    ∀ (x : ↥(inertiaInvariants A (N * q)))
      (hx : heckeGen ℓ • (x : JZero (N * q)) ∈ inertiaInvariants A (N * q)),
      comp x = 0 → GluedPic0.toPic0Pair nodes (sp ⟨heckeGen ℓ • (x : JZero (N * q)), hx⟩) =
        heckeGen ℓ • GluedPic0.toPic0Pair nodes (sp x)

  toPic0Pair_sp_eq_zero : ∀ (T : HeckeAlg) (x : ↥(inertiaInvariants A (N * q)))
      (hx : T • (x : JZero (N * q)) ∈ inertiaInvariants A (N * q)),
      comp x = 0 → GluedPic0.toPic0Pair nodes (sp x) = 0 →
        GluedPic0.toPic0Pair nodes (sp ⟨T • (x : JZero (N * q)), hx⟩) = 0

  sp_frob : ∀ φ : Qbar ≃ₐ[ℚ] Qbar, A.IsFrobeniusAt φ q →
    ∀ (x : ↥(inertiaInvariants A (N * q)))
      (hx : φ • (x : JZero (N * q)) ∈ inertiaInvariants A (N * q)),
      comp x = 0 → sp ⟨φ • (x : JZero (N * q)), hx⟩ =
        GluedPic0.glueMap nodes frob frob_nodeStable (sp x)

  sp_heckeGen_self : ∀ (x : ↥(inertiaInvariants A (N * q)))
      (hx : heckeGen ⟨q, hq⟩ • (x : JZero (N * q)) ∈ inertiaInvariants A (N * q)),
      comp x = 0 → ∀ w : ↥nodes → Additive (ResidueField A)ˣ,
        sp x = GluedPic0.nodeUnit nodes w →
          sp ⟨heckeGen ⟨q, hq⟩ • (x : JZero (N * q)), hx⟩ = GluedPic0.nodeUnit nodes
            (fun t => w ((SemilinearAut.nodePerm nodes frob frob_nodeStable).symm t))

  sp_injective : ∀ x : ↥(inertiaInvariants A (N * q)),
    PrimeToTorsion q (x : JZero (N * q)) → comp x = 0 → sp x = 0 → x = 0

  exists_prime_torsion : ∀ 𝔪 : Ideal HeckeAlg, 𝔪.IsMaximal → IsUnit ((q : ℕ) : HeckeAlg ⧸ 𝔪) →
    ∀ x ∈ heckeTorsion (JZero (N * q)) 𝔪, ∃ p : ℕ, p.Prime ∧ p ≠ q ∧ p • x = 0

  spN : JZero N →+ Pic0 (ResidueField A) (modularFunctionFieldC (ResidueField A) N)

  spN_hecke : ∀ (T : HeckeAlg) (y : JZero N), spN (T • y) = T • spN y

  spN_injective : ∀ y : JZero N, PrimeToTorsion q y → spN y = 0 → y = 0

  spN_surjective : ∀ c : Pic0 (ResidueField A) (modularFunctionFieldC (ResidueField A) N),
    PrimeToTorsion q c → ∃ y : JZero N, PrimeToTorsion q y ∧ spN y = c

end Semistable

end ModularCurve

end

Statements phrased using this module (128)