Definitions/Def_AutomorphicForm_CyclicBaseChangeLifting.lean

For number fields F and E with E an F-algebra, and for a parameter notion : CuspidalityNotion ℂ (a structure whose single field assigns to every number field K a predicate IsCusp on complex Hecke eigensystems over K), this module defines the Prop-valued structure LanglandsLiftingProperties, a four-field package of the lifting and descent properties of cyclic base change, formulated entirely in terms of Satake data. Here a Hecke eigensystem over K consists of a nonzero level ideal of \mathcal O_K together with two functions a, b from the height-one spectrum of \mathcal O_K to the coefficient ring; \pi base changes to \Psi (IsBaseChangeOf) when, outside some finite set of primes \mathfrak P of \mathcal O_E, one has \Psi.a(\mathfrak P) = \mathrm{satakePow}_f(\pi.a(v), \pi.b(v)) and \Psi.b(\mathfrak P) = \pi.b(v)^f, where v is the prime of \mathcal O_F under \mathfrak P, f is its residue degree, and \mathrm{satakePow}_n(s,e) is the recursion 2, s, s\,\mathrm{satakePow}_{n+1} - e\,\mathrm{satakePow}_n computing the trace of the n-th power of a matrix of trace s and determinant e.

The fields are: propertyA, every cuspidal \pi over F admits some \Psi over E with \pi base changing to \Psi (no cuspidality demanded of \Psi); propertyB, every cuspidal \Psi over E which is constant on fibres over F (that is, outside a finite set of primes, a and b agree at any two primes of \mathcal O_E lying over the same prime of \mathcal O_F with the same residue degree) is the base change of some cuspidal \pi over F; propertyC, if cuspidal \pi, \pi' over F both base change to the same \Psi, then there are a modulus \mathfrak f admissible for E/F (nonzero, and divisible by v^{4e_2+2e_3+1}, with e_2, e_3 the ramification indices of (2) and (3) at v, for every prime v whose chosen prime above in E has nontrivial inertia) and a character \omega of the narrow ray class group modulo \mathfrak f with values in \mathbb C^\times, trivial on the f(w/v)-th power of the class of v for every prime w of \mathcal O_E over a prime v \nmid \mathfrak f, such that outside a finite set of primes v \nmid \mathfrak f one has \pi'.a(v) = \omega([v])\,\pi.a(v) and \pi'.b(v) = \omega([v])^2\,\pi.b(v), i.e. \pi' is the twist of \pi by \omega away from finitely many primes; propertyG, which spells out the existential in IsBaseChangeOf and therefore asks nothing beyond its hypothesis. The structure has no field asserting the classical pointwise strong multiplicity one property.