Definitions/Def_AutomorphicForm_DihedralWeightOneLift.lean

Working over the rational field, this module sets up the shape of the adelization of a weight-one form on the upper half plane. First, DihedralWeightOne.weightOneArchLift takes a function f : \mathbb{H} \to \mathbb{C} and an element h \in \mathrm{GL}_2(\mathbb{R}) and returns (f \mid_1 h)(i) \cdot (\det h)^{1}, where \mid_1 is the weight-one slash action, the value is read at the point i of the upper half plane, and the determinant (a unit of \mathbb{R}) is coerced into \mathbb{C} and raised to the integer power 1. Second, DihedralWeightOne.HasWeightOneDecomp is a predicate on an ideal N of the ring of integers of \mathbb{Q} and an element g of \mathrm{GL}_2 of the adele ring: it asserts the existence of \gamma \in \mathrm{GL}_2(\mathbb{Q}) and adelic elements h, u with u in the level-N subgroup (\mathtt{productionPinsCompact}\ \mathbb{Q}).U\,N, which by definition is the intersection of the level-one subgroup attached to N with the kernel of the archimedean projection, with h trivial at all finite places (AdelicLevel.glFin of h equal to 1), with the associated real matrix LanglandsTunnell.ratArchGL2 h — the component of h at the unique infinite place of \mathbb{Q}, transported along the identification of that completion with \mathbb{R} — of positive determinant, and with g = \gamma h u, the global point \gamma being taken in the adelic group by AutomorphicForm.globalPoints. Third, DihedralWeightOne.weightOneLift N f g is defined by a case split on this predicate: where a decomposition exists, it is the archimedean lift of f evaluated at the real matrix attached to the middle factor of a classically chosen witness; where none exists, the value is 0. Thus the definition as such carries no invariance, eigenfunction or well-definedness assertion: independence of the choice of decomposition and the automorphy properties are the content of separate theorems.