Descent of a signed eigenline to algebraic coefficients

Proved

MTT.Cohomology.eigenclass_descent

by davidloeffler · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

group-cohomologymodular-formsperiods

Given integral finite generation, the two canonical base-change isomorphisms, and dimension at most one for a signed algebraic Hecke eigenpacket, every complex class in that packet is a nonzero complex scalar times a coefficientwise algebraic class. The zero class is allowed and may use scalar 1. This is finite-dimensional linear algebra applied to the explicitly defined algebraic Hecke, nebentype and sign equations; it assumes no period theorem.

Preamble

import Definitions.Def_MTT_Cohomology
import Mathlib.RingTheory.Flat.Basic
set_option autoImplicit false
noncomputable section
open scoped BigOperators TensorProduct
open MTT.Cohomology

Formal statement

theorem MTT.Cohomology.eigenclass_descent
    {N n : ℕ} (hZ : Module.Finite ℤ (Hc N n ℤ))
    (hQ : BaseChange N n MTT.Qbar) (hC : BaseChange N n ℂ)
    (ι : MTT.Qbar →+* ℂ) (e : DirichletCharacter MTT.Qbar N)
    (a : ℕ → MTT.Qbar) (s : Bool)
    (hdim : ∀ φ ψ : Hc N n ℂ,
      Packet (fun d => ι (e d)) (fun l => ι (a l)) s φ →
      Packet (fun d => ι (e d)) (fun l => ι (a l)) s ψ →
      ∃ u v : ℂ, (u ≠ 0 ∨ v ≠ 0) ∧ u • φ + v • ψ = 0)
    (φ : Hc N n ℂ)
    (hφ : Packet (fun d => ι (e d)) (fun l => ι (a l)) s φ) :
    ∃ ω : ℂ, ω ≠ 0 ∧ ∃ ψ : Hc N n MTT.Qbar, Extends ι ψ (ω⁻¹ • φ) := by sorry

Source

Elementary descent of kernels of algebraic linear equations; compare Williams §11.5–11.6, especially Lemma 11.16 and the eigenline argument leading to Proposition 11.19. https://warwick.ac.uk/fac/sci/maths/people/staff/cwilliams/lecturenotes/lecture_notes_part_ii.pdf

View graph