Definitions/Def_LanglandsTunnell_CubicInduction_KFinite3.lean

Three notions attached to a complex-valued function f on \mathrm{GL}_3 of the adeles of \mathbb{Q} are defined here. Let \mathcal{K} denote the set of adelic matrices k whose component componentAt3 at every nonzero prime p of \mathbb{Z} is the identity and whose archimedean component archComponent3 lies in orth3, the set of k over the infinite adeles of \mathbb{Q} with k^{\mathsf{T}}k = 1. First, IsOrthFinite f asserts the existence of a single finite set s of functions on adelic \mathrm{GL}_3 such that for every k \in \mathcal{K} the right translate g \mapsto f(gk) lies in the \mathbb{C}-span of s; equivalently, the translates of f by \mathcal{K} span a finite-dimensional space. Second, orthSpan f is that span itself: the \mathbb{C}-submodule of all functions on adelic \mathrm{GL}_3 generated by the functions g \mapsto f(gk) for k \in \mathcal{K}. Third, gKSpan f is the submodule of smoothFunctions3 — the \mathbb{C}-submodule of functions \varphi satisfying IsArchSmooth3, i.e. for each g the map e \mapsto \varphi(g\cdot\,archRealLift3\,e) is C^\infty on the open set of real 3\times 3 entry arrays of nonzero determinant — generated over envelopingAlgebra3, the universal enveloping algebra of \mathfrak{gl}_3(\mathbb{C}) (the matrix algebra with its commutator bracket), by those smooth functions whose underlying function lies in orthSpan f. The enveloping-algebra action is the one determined by derivAction3, which sends the matrix unit E_{ij} to the right derivative archDerivₗ i j in the archimedean direction 1 + sE_{ij}; that this is a Lie algebra homomorphism is derivAction3_lie, and envelopingHom3 is its extension to the enveloping algebra.