Definitions/Def_AutomorphicForm_ViaCompactCuspNotion.lean

Four things are set up here. First, iotaZsqrtdNegTwo is the fixed ring homomorphism \mathbb{Z}[\sqrt{-2}]\to\mathbb{C} obtained from Zsqrtd.lift by sending the generator to \sqrt2\,i; iotaZsqrtdNegTwo_apply records that z\mapsto z_{\mathrm{re}}+z_{\mathrm{im}}\sqrt2\,i. Second, iwasawaSectionGL sends z in the upper half-plane to the matrix \begin{pmatrix}\operatorname{Im}z&\operatorname{Re}z\\0&1\end{pmatrix}\in GL_2(\mathbb{R}) (invertible since \operatorname{Im}z\neq0), the usual section of GL_2(\mathbb{R})\to\mathfrak{H} at i. Third, IsArchHolomorphicAt w hw φ, for a real infinite place w of a number field F and φ\colon GL_2(\mathbb{A}_F)\to\mathbb{C}, asserts that for every g the function z\mapsto(\operatorname{Im}z)^{-1}\,φ\bigl(g\cdot\iota_w(s_z)\bigr) is MDifferentiable for the model \mathcal{I}(\mathbb{C}) on the upper half-plane, where s_z is the above section transported to GL_2(F_w) along the inverse of the isometric isomorphism F_w\cong\mathbb{R} and \iota_w is the inclusion of the w-component into the adelic group; so the normalised Iwasawa descent of φ at w is holomorphic.

Fourth, viaCompactCuspNotion is an element of the project's CuspidalityNotion over \mathbb{Z}[\sqrt{-2}]: for Φ a Hecke eigensystem over F with coefficients in \mathbb{Z}[\sqrt{-2}], IsCusp F Φ is the conjunction of (i) the existence of a single witness R in the project's structure SmoothCuspRealizationAt at the pins productionPinsCompact F for the rescaled eigensystem (Φ\circ\iota_0)^{\mathrm{raw}} (in which b_v is divided by \lvert N v\rvert) whose underlying function satisfies, at every real place w, both the weight-one archimedean character condition HasArchCharacterAt₀ F w (archWeightOneAt hw) — equivariance φ(g\,\iota_w(k))=\chi(k)φ(g) for k in the determinant-one row-isometry subgroup, with \chi the transported character k\mapsto k_{00}+ik_{01} — and IsArchHolomorphicAt w hw; and (ii) the existence of a finite set S of finite places with Φ.b\,v=\chi_{-3}(N v) for v\notin S, where \chi_{-3}(n) is 1,-1,0 according as n\equiv1,2,0\pmod 3. Note that (i) demands one joint witness, not a property of all realisations, and that complex places are unconstrained. viaCompactCuspNotion_isCusp_iff is this unfolding by Iff.rfl, and isArithCuspRealizableVia_of_viaCompactCuspNotion extracts from IsCusp the weaker statement IsArithCuspRealizableVia F (productionPinsCompact F) iotaZsqrtdNegTwo Φ, i.e. mere nonemptiness of the realisation type, by forgetting the archimedean clauses.