`Definitions/Def_LanglandsTunnell_LiftTraceSeed.lean`

definition module

Seed Hecke eigensystem from an explicit lift of $GL_{2} (F_{3})$

Throughout, L is a number field, H a subgroup of L \simeq_{\mathbb{Q}} L, and F = L^H the associated fixed intermediate field FixedPoints.intermediateField H. Four groups of definitions are made. First, for a finite group G, a subgroup H and \sigma \in G, exists_pos_pow_mem records that some positive power of \sigma lies in H (take the order of \sigma), and relDeg H \sigma is the least such positive exponent. Second, algebraMap_ringOfIntegers_injective gives injectivity of \mathcal{O}_F \to \mathcal{O}_L, and exists_prime_over produces, for each w in the height-one spectrum of \mathcal{O}_F, a maximal ideal of \mathcal{O}_L contracting to w; primeOver H w is a choice of such an ideal, with the accompanying facts that it is maximal, contracts to w, is nonzero, and has finite residue ring. Third, for L/\mathbb{Q} Galois, seedFrob H w is the arithmetic Frobenius arithFrobAt at primeOver H w, raised to its relative degree with respect to H; thus it lies in H by construction of relDeg. Fourth, liftOf g, for g \in \mathrm{GL}_2(\mathbb{Z}/3), is an element of \mathrm{M}_2(\mathbb{Z}[\sqrt{-2}]) selected by Hilbert's epsilon operator from those matrices lying in the submonoid generated by the explicit matrices Slift, Tlift whose entrywise image under red (the ring map \mathbb{Z}[\sqrt{-2}] \to \mathbb{Z}/3 sending \sqrt{-2} \mapsto -1) equals g; no existence or uniqueness is asserted at this point. Finally, given a group isomorphism e from L \simeq_{\mathbb{Q}} L to \mathrm{GL}_2(\mathbb{Z}/3), liftTraceSeed e H is the record over F with coefficients \mathbb{Z}[\sqrt{-2}] consisting of the unit ideal as level, together with the two functions w \mapsto \operatorname{tr} and w \mapsto \det of liftOf (e (seedFrob H w)).

Relation to Mathlib

AutomorphicForm.HeckeEigensystem is the project's own bookkeeping record — a nonzero level ideal together with two coefficient functions on the height-one spectrum — and carries no analytic content; Mathlib has no such notion. The remaining ingredients (Nat.find, existence of primes over a maximal ideal in an integral extension, arithFrobAt, Zsqrtd) are Mathlib's.

Where it is used

This seed system is the starting point of the Langlands–Tunnell input to modularity of the mod 3 representation: its coefficients are traces and determinants of the canonical lift to \mathrm{GL}_2(\mathbb{Z}[\sqrt{-2}]) of Frobenius elements, over the fixed field of a subgroup H of the Galois group cut out by the representation, and it is the object to which cyclic base change and descent are applied.

References

R. P. Langlands, Base Change for GL(2), Annals of Mathematics Studies 96, Princeton University Press, 1980
J. Tunnell, Artin's conjecture for representations of octahedral type, Bulletin of the American Mathematical Society (N.S.) 5 (1981), 173–175

References are suggested automatically and have not been individually verified.

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

103 lines
12 declarations
used in the statements of 14 theorems and imported by 16 proofs
imports 2 definition modules

Source file: Definitions/Def_LanglandsTunnell_LiftTraceSeed.lean

Imports

Imported by

Def_LanglandsTunnell_C8Character

Declarations

theoremLanglandsTunnell.P2.exists_pos_pow_mem
defLanglandsTunnell.P2.relDeg
theoremLanglandsTunnell.P2.algebraMap_ringOfIntegers_injective
theoremLanglandsTunnell.P2.exists_prime_over
defLanglandsTunnell.P2.primeOver
instanceLanglandsTunnell.P2.primeOver_isMaximal
theoremLanglandsTunnell.P2.under_primeOver
theoremLanglandsTunnell.P2.primeOver_ne_bot
instanceLanglandsTunnell.P2.primeOver_finite
defLanglandsTunnell.P2.seedFrob
defLanglandsTunnell.P2.liftOf
defLanglandsTunnell.P2.liftTraceSeed

Source

import Definitions.Def_AutomorphicForm_HeckeEigensystem
import Definitions.Def_LanglandsTunnell_ExplicitLift

set_option autoImplicit false

noncomputable section

namespace LanglandsTunnell.P2

open NumberField IsDedekindDomain FLT.ExplicitLift

section RelDeg

variable {G : Type*} [Group G] [Finite G] (H : Subgroup G) (σ : G)

theorem exists_pos_pow_mem : ∃ n : ℕ, 0 < n ∧ σ ^ n ∈ H :=
  ⟨orderOf σ, orderOf_pos σ, by rw [pow_orderOf_eq_one]; exact H.one_mem⟩

open Classical in

def relDeg : ℕ := Nat.find (exists_pos_pow_mem H σ)

end RelDeg

section PrimeOver

variable {L : Type*} [Field L] [NumberField L] (H : Subgroup (L ≃ₐ[ℚ] L))

theorem algebraMap_ringOfIntegers_injective :
    Function.Injective (algebraMap (𝓞 (FixedPoints.intermediateField H : IntermediateField ℚ L)) (𝓞 L)) := by
  intro x y h
  have h' : algebraMap (𝓞 (FixedPoints.intermediateField H : IntermediateField ℚ L)) L x
      = algebraMap (𝓞 (FixedPoints.intermediateField H : IntermediateField ℚ L)) L y := by
    rw [IsScalarTower.algebraMap_apply (𝓞 (FixedPoints.intermediateField H : IntermediateField ℚ L)) (𝓞 L) L,
      IsScalarTower.algebraMap_apply (𝓞 (FixedPoints.intermediateField H : IntermediateField ℚ L)) (𝓞 L) L, h]
  rw [IsScalarTower.algebraMap_apply (𝓞 (FixedPoints.intermediateField H : IntermediateField ℚ L))
      (FixedPoints.intermediateField H : IntermediateField ℚ L) L,
    IsScalarTower.algebraMap_apply (𝓞 (FixedPoints.intermediateField H : IntermediateField ℚ L))
      (FixedPoints.intermediateField H : IntermediateField ℚ L) L] at h'
  exact IsFractionRing.injective (𝓞 (FixedPoints.intermediateField H : IntermediateField ℚ L))
    (FixedPoints.intermediateField H : IntermediateField ℚ L) ((algebraMap _ L).injective h')

theorem exists_prime_over (w : HeightOneSpectrum (𝓞 (FixedPoints.intermediateField H : IntermediateField ℚ L))) :
    ∃ Q : Ideal (𝓞 L), Q.IsMaximal ∧ Q.under (𝓞 (FixedPoints.intermediateField H : IntermediateField ℚ L)) = w.asIdeal := by
  haveI := w.isMaximal
  obtain ⟨Q, hQ, hQw⟩ := Ideal.exists_ideal_over_maximal_of_isIntegral w.asIdeal
    (by rw [(RingHom.injective_iff_ker_eq_bot _).mp (algebraMap_ringOfIntegers_injective H)]; exact bot_le)
  exact ⟨Q, hQ, hQw⟩

def primeOver (w : HeightOneSpectrum (𝓞 (FixedPoints.intermediateField H : IntermediateField ℚ L))) : Ideal (𝓞 L) :=
  (exists_prime_over H w).choose

variable (w : HeightOneSpectrum (𝓞 (FixedPoints.intermediateField H : IntermediateField ℚ L)))

instance primeOver_isMaximal : (primeOver H w).IsMaximal := (exists_prime_over H w).choose_spec.1

theorem under_primeOver :
    (primeOver H w).under (𝓞 (FixedPoints.intermediateField H : IntermediateField ℚ L)) = w.asIdeal :=
  (exists_prime_over H w).choose_spec.2

theorem primeOver_ne_bot : primeOver H w ≠ ⊥ := fun h => by
  have := under_primeOver H w
  rw [h, Ideal.under_def, Ideal.comap_bot_of_injective _ (algebraMap_ringOfIntegers_injective H)] at this
  exact w.ne_bot this.symm

instance primeOver_finite : Finite (𝓞 L ⧸ primeOver H w) :=
  Ideal.finiteQuotientOfFreeOfNeBot _ (primeOver_ne_bot H w)

end PrimeOver

section Frob

variable {L : Type*} [Field L] [NumberField L] [IsGalois ℚ L] (H : Subgroup (L ≃ₐ[ℚ] L))
  (w : HeightOneSpectrum (𝓞 (FixedPoints.intermediateField H : IntermediateField ℚ L)))

def seedFrob : L ≃ₐ[ℚ] L :=
  arithFrobAt ℤ (L ≃ₐ[ℚ] L) (primeOver H w) ^ relDeg H (arithFrobAt ℤ (L ≃ₐ[ℚ] L) (primeOver H w))

end Frob

section Seed

def liftOf (g : Matrix.GeneralLinearGroup (Fin 2) (ZMod 3)) : Matrix (Fin 2) (Fin 2) (ℤ√(-2)) :=
  Classical.epsilon fun M : Matrix (Fin 2) (Fin 2) (ℤ√(-2)) =>
    M ∈ Submonoid.closure ({Slift, Tlift} : Set (Matrix (Fin 2) (Fin 2) (ℤ√(-2)))) ∧
      M.map red = (g : Matrix (Fin 2) (Fin 2) (ZMod 3))

variable {L : Type*} [Field L] [NumberField L] [IsGalois ℚ L]
  (e : (L ≃ₐ[ℚ] L) ≃* Matrix.GeneralLinearGroup (Fin 2) (ZMod 3)) (H : Subgroup (L ≃ₐ[ℚ] L))

def liftTraceSeed :
    AutomorphicForm.HeckeEigensystem (FixedPoints.intermediateField H : IntermediateField ℚ L) (ℤ√(-2)) where
  level := ⊤
  level_ne_bot := top_ne_bot
  a := fun w => (liftOf (e (seedFrob H w))).trace
  b := fun w => (liftOf (e (seedFrob H w))).det

end Seed

end LanglandsTunnell.P2

end

Definitions/Def_LanglandsTunnell_LiftTraceSeed.lean

Seed Hecke eigensystem from an explicit lift of GL2​(F3​)