Definitions/Def_LanglandsTunnell_IsAttached.lean

Working with the Galois group written as the group of \mathbb{Q}-algebra automorphisms of \overline{\mathbb{Q}} = AlgebraicClosure ℚ, this module defines three predicates comparing a homomorphism \rho of that group into \mathrm{GL}_2(\mathbb{Z}/3) with a Hecke eigensystem \pi_0 of type HeckeEigensystem ℚ (ℤ√(-2)) — that is, a nonzero ideal level of \mathcal{O}_{\mathbb{Q}} together with two functions a, b from the height-one spectrum of \mathcal{O}_{\mathbb{Q}} to \mathbb{Z}[\sqrt{-2}] — away from a finite set T of natural numbers. IsAttachedExact ρ π₀ T asserts: for every prime p with p \notin T, every valuation subring A of \overline{\mathbb{Q}} with p a nonunit of A, and every \sigma lying in the decomposition subgroup of A over \mathbb{Q} and inducing x \mapsto x^p on the residue field of A, one has \mathrm{red}(\pi_0.a(v_p)) = \mathrm{tr}\,\rho(\sigma) in \mathbb{Z}/3, where v_p is the place of \mathcal{O}_{\mathbb{Q}} corresponding to p under Rat.HeightOneSpectrum.primesEquiv, \mathrm{red} : \mathbb{Z}[\sqrt{-2}] \to \mathbb{Z}/3 is the ring homomorphism sending \sqrt{-2} to -1, and the trace is that of the underlying 2 \times 2 matrix. IsAttachedTwisted has the same shape with the right-hand side multiplied by the image in \mathbb{Z}/3 of chiNegThree p, i.e. of 1, -1 or 0 according as p \equiv 1, 2, 0 \pmod 3. IsAttachedUpToTwist is the disjunction of the two, the choice of branch being made once and for all, outside the quantifier over places. These are congruences of traces in characteristic 3 at unramified-type data only: no continuity, irreducibility or automorphy is asserted, and no characteristic-zero identity. The accompanying lemma isAttachedUpToTwist_one exhibits one instance of the untwisted branch, for trivial \rho, empty T and the eigensystem with unit level and constant data a \equiv 2, b \equiv 0, where both sides equal 2.