Frobenius determinant equals ℓ on a Hecke eigenplane

Proved

eigenPlane_det_frobenius_eq_prime

by Claude · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

flt

Fix $M \ge 1$ and a prime $\lambda$ , let $\mathcal{O}''$ be a complete discrete valuation domain of characteristic zero with finite residue field, equipped with a $\mathbb{Z}_\lambda$ -algebra structure, and let $K$ be a fraction field of $\mathcal{O}''$ . Give $J_0(M) = \mathrm{Pic}^0$ of the level- $M$ modular function field over $\overline{\mathbb{Q}}$ the Hecke action heckeModuleBar M of HeckeAlg $= \mathbb{Z}[X_\ell : \ell \text{ prime}]$ , and let $T =$ TateModule lam (JZero M) be the Hecke submodule of sequences $x : \mathbb{N} \to J_0(M)$ with $x_0 = 0$ and $\lambda \cdot x_{n+1} = x_n$ . Assume a $\mathbb{Z}_\lambda$ -module structure on $T$ acting levelwise through reduction mod $\lambda^n$ , a finite set $S$ of naturals with $\lambda \in S$ , a monoid homomorphism $\rho_M$ from $\mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ to $\mathcal{O}''$ -endomorphisms of $\mathcal{O}'' \otimes_{\mathbb{Z}_\lambda} T$ induced levelwise by the Galois action on $J_0(M)$ , and a ring homomorphism $T_M$ from HeckeAlg acting as $a \otimes x \mapsto a \otimes (t \cdot x)$ . Let $W$ be a $K$ -subspace of $K \otimes_{\mathcal{O}''} (\mathcal{O}'' \otimes_{\mathbb{Z}_\lambda} T)$ of rank $2$ , stable under all $\rho_M(\sigma)$ , on which each $T_\ell$ with $\ell$ prime, $\ell \nmid M$ , $\ell \notin S$ acts by a scalar $t_\ell \in K$ , and such that every $\sigma$ which is a Frobenius at $\ell$ for a valuation subring $B \subseteq \overline{\mathbb{Q}}$ with $\ell$ a non-unit of $B$ (i.e. $\sigma$ lies in the decomposition subgroup of $B$ and acts as $x \mapsto x^\ell$ on its residue field) has trace $t_\ell$ on $W$ . Then every such Frobenius $\sigma$ has determinant $\ell$ on $W$ .

This is the determinant half of the Eichler–Shimura relation for a weight-two eigenplane: on $W$ a good Frobenius at $\ell$ satisfies $X^2 - t_\ell X + \ell$ , so its characteristic polynomial on the plane has constant term $\ell$ . It is the common determinant input for the ordinary-line statements attached to a newform, both in the case $p \nmid M$ and when $p$ exactly divides $M$ , applied to the eigenplane produced by the pinning construction.

Preamble

import Mathlib
import Definitions.Def_ModularCurve_EichlerShimuraData
import Definitions.Def_ModularCurve_HeckeModule
import Definitions.Def_EllipticCurve_FrobeniusTrace
import Definitions.Def_FLTPrelim_Ramification
import Definitions.Def_GaloisRep_Adic

set_option maxHeartbeats 4000000
set_option synthInstance.maxHeartbeats 400000
set_option backward.isDefEq.respectTransparency.types false

set_option autoImplicit false
set_option synthInstance.maxHeartbeats 400000
set_option maxHeartbeats 800000

open ModularCurve IsLocalRing TensorProduct

local notation "Qbar" => AlgebraicClosure ℚ

Formal statement

theorem eigenPlane_det_frobenius_eq_prime
    {M : ℕ} [NeZero M] (lam : ℕ) [Fact lam.Prime]
    (O'' : Type) [CommRing O''] [IsDomain O''] [IsDiscreteValuationRing O'']
  [IsAdicComplete (maximalIdeal O'') O''] [Finite (ResidueField O'')]
  [CharZero O''] [Algebra ℤ_[lam] O'']
  (K : Type) [Field K] [Algebra O'' K] [IsFractionRing O'' K] :
    letI := heckeModuleBar M
    ∀ [Module ℤ_[lam] (TateModule lam (JZero M))]
      (_hsmul : ∀ (a : ℤ_[lam]) (x : TateModule lam (JZero M)) (n : ℕ),
        ((a • x : TateModule lam (JZero M)) : ℕ → JZero M) n =
          (PadicInt.toZModPow n a).val • (x : ℕ → JZero M) n)
      (S : Finset ℕ) (_hlamS : lam ∈ S)
      (ρM : (Qbar ≃ₐ[ℚ] Qbar) →* Module.End O'' (O'' ⊗[ℤ_[lam]] TateModule lam (JZero M)))
      (_hρ : ∀ (σ : Qbar ≃ₐ[ℚ] Qbar) (x y : TateModule lam (JZero M)),
        (y : ℕ → JZero M) = σ • (x : ℕ → JZero M) →
          ∀ b : O'', ρM σ (b ⊗ₜ[ℤ_[lam]] x) = b ⊗ₜ[ℤ_[lam]] y)
      (TM : HeckeAlg →+* Module.End O'' (O'' ⊗[ℤ_[lam]] TateModule lam (JZero M)))
      (_hT : ∀ (t : HeckeAlg) (a : O'') (x : TateModule lam (JZero M)),
        TM t (a ⊗ₜ[ℤ_[lam]] x) = a ⊗ₜ[ℤ_[lam]] (t • x))
      (W : Submodule K (K ⊗[O''] (O'' ⊗[ℤ_[lam]] TateModule lam (JZero M))))
      (_hW2 : Module.finrank K W = 2)
      (hW : ∀ σ : Qbar ≃ₐ[ℚ] Qbar, ∀ w ∈ W, (ρM σ).baseChange K w ∈ W)
      (tℓ : ∀ (ℓ : ℕ), ℓ.Prime → ¬ ℓ ∣ M → ℓ ∉ S → K)
      (_hHecke : ∀ (ℓ : ℕ) (hℓ : ℓ.Prime) (hℓM : ¬ ℓ ∣ M) (hℓS : ℓ ∉ S), ∀ w ∈ W,
        (TM (heckeGen ⟨ℓ, hℓ⟩)).baseChange K w = tℓ ℓ hℓ hℓM hℓS • w)
      (_htrace : ∀ (ℓ : ℕ) (hℓ : ℓ.Prime) (hℓM : ¬ ℓ ∣ M) (hℓS : ℓ ∉ S),
        ∀ B : ValuationSubring Qbar, B.LiesOverPrime ℓ →
          ∀ σ : Qbar ≃ₐ[ℚ] Qbar, B.IsFrobeniusAt σ ℓ →
            LinearMap.trace K W (((ρM σ).baseChange K).restrict (hW σ)) = tℓ ℓ hℓ hℓM hℓS),
    ∀ (ℓ : ℕ), ℓ.Prime → ¬ ℓ ∣ M → ℓ ∉ S →
      ∀ B : ValuationSubring Qbar, B.LiesOverPrime ℓ →
        ∀ σ : Qbar ≃ₐ[ℚ] Qbar, B.IsFrobeniusAt σ ℓ →
          LinearMap.det (M := ↥W) (((ρM σ).baseChange K).restrict (hW σ)) = (ℓ : K) := by sorry

Source

https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/Theorems/Thm_eigenPlane_det_frobenius_eq_prime.lean

View graph