Definitions/Def_LanglandsTunnell_TunnellExistenceCarriers.lean

Three propositions are defined, each parametrised by one or two cuspidality notions: a CuspidalityNotion R is a structure whose single field is a family of predicates IsCusp on Hecke eigensystems over arbitrary number fields, so no intrinsic cuspidality is assumed; here the coefficient ring is \mathbb{Z}[\sqrt{-2}]. A HeckeEigensystem F R is a nonzero level ideal of \mathcal{O}_F together with two functions a,b on the finite places, and AgreesAwayFromFinite means the two pairs (a_v,b_v) coincide outside some finite set of places.

TunnellExistsForAttachedOctahedralData notionT asserts: for every continuous surjective monoid homomorphism \rho:\mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})\to \mathrm{GL}_2(\mathbb{Z}/3) with \det\rho(\sigma) equal to the mod-3 cyclotomic character for all \sigma, every linked octahedral Galois datum D over \mathbb{Q} (a finite group G with a surjection onto \mathrm{Perm}(\mathrm{Fin}\,4) whose kernel is exactly the locus where a given G\to\mathrm{GL}_2(\mathbb{Z}[\sqrt{-2}]) is scalar, a Frobenius assignment v\mapsto\mathrm{frob}(v), a finite ramified set, and an eigensystem attached whose a_v,b_v are the trace and determinant of \mathrm{rep}(\mathrm{frob}(v)) outside it), and every finite S\subseteq\mathbb{N} such that D is a Galois attachment of \rho off S (i.e. for p\notin S and every Frobenius \sigma at p, the image of a_p under the ring map \mathbb{Z}[\sqrt{-2}]\to\mathbb{Z}/3, \sqrt{-2}\mapsto-1, equals \operatorname{tr}\rho(\sigma)), there is a notionT-cuspidal eigensystem over \mathbb{Q} agreeing with D.attached away from finitely many places.

NotionInhabitedOverRat notionD asserts that some eigensystem over \mathbb{Q} is notionD-cuspidal. NotionCompatForAttachedOctahedralData notionT notionD asserts, under the same hypotheses on \rho,D,S, that any notionT-cuspidal eigensystem agreeing almost everywhere with D.attached is notionD-cuspidal. Thus the classical theorem is reformulated at the level of Satake data (a_v,b_v) up to finitely many places, with cuspidality left as a parameter.