Definitions/Def_AutomorphicForm_HeckeEigensystemMap.lean

Fix a number field F. The project's structure HeckeEigensystem F R, for a commutative ring R, is purely bookkeeping data: an ideal \mathrm{level} \subseteq \mathcal{O}_F together with a proof that it is nonzero, and two arbitrary families a, b : \mathrm{Spec}^1(\mathcal{O}_F) \to R indexed by the height-one primes of \mathcal{O}_F (intended as the T_v- and S_v-eigenvalues); no automorphy, no Euler-product or local condition is imposed. This module defines the transport of such data along a ring homomorphism \iota : R \to S: AutomorphicForm.HeckeEigensystem.map ι Φ has the same level ideal (and the same nonvanishing proof) and has Satake data v \mapsto \iota(a_\Phi(v)) and v \mapsto \iota(b_\Phi(v)). Three lemmas map_level, map_a, map_b record these three components.

The remaining declarations are the functoriality and compatibility interface. map_id says transport along the identity homomorphism of R returns \Phi itself (by structure eta), and map_map says that transporting along \iota : R \to S and then along \kappa : S \to T agrees with transporting along \kappa \circ \iota. map_twist compares transport with the twisting operation \Phi \mapsto \Phi.\mathrm{twist}\,\chi defined by a \mapsto \chi(v)a_\Phi(v), b \mapsto \chi(v)^2 b_\Phi(v) for an arbitrary family \chi : \mathrm{Spec}^1(\mathcal{O}_F) \to R: transporting a twist equals twisting the transport by \iota \circ \chi, which uses only multiplicativity of \iota (and \iota(x^2) = \iota(x)^2). Finally AgreesAwayFromFinite.map shows that the relation '\Phi and \Phi' have equal a- and b-values at all primes outside some finite set' is preserved by transport, with literally the same exceptional finite set. No hypothesis of injectivity, continuity or integrality on \iota occurs, and nothing is asserted about existence or automorphy of eigensystems.