Definitions/Def_AutomorphicForm_ComplexIwasawa.lean

Fix a matrix g \in M_2(\mathbb{C}), with entries written a = g_{00}, b = g_{01}, c = g_{10}, d = g_{11} in the Fin 2 indexing, and let z \in \mathbb{C}. The module introduces four explicit coordinate functions attached to the pair (g,z). First, botP g z is the complex number P = a + zc and botQ g z is Q = b + zd; these are the two entries of the bottom row of the product \begin{pmatrix}0&1\\1&0\end{pmatrix}\begin{pmatrix}1&z\\0&1\end{pmatrix} g, that is, of \begin{pmatrix} c & d \\ a+zc & b+zd\end{pmatrix}. Second, radC g z is the non-negative real number r = \sqrt{\lvert P\rvert^2 + \lvert Q\rvert^2}, defined as Real.sqrt applied to the sum of the squared norms Complex.normSq (botP g z) and Complex.normSq (botQ g z). Third, kC g z is the explicit 2\times2 complex matrix \begin{pmatrix} \overline{Q}/r & -\overline{P}/r \\ P/r & Q/r \end{pmatrix}, where each division is division in \mathbb{C} by the coercion of the real number r. All four declarations are plain definitions: no non-degeneracy hypothesis on g is imposed, and no property is asserted. In particular, nothing here claims that r > 0, that kC g z is unitary of determinant one, or that \begin{pmatrix}0&1\\1&0\end{pmatrix}\begin{pmatrix}1&z\\0&1\end{pmatrix} g equals an upper-triangular matrix times kC g z; such facts, which require \det g \neq 0, are theorems elsewhere about these coordinates. Where r = 0 (possible only when P = Q = 0), division by zero in \mathbb{C} returns 0, so every entry of kC g z is then 0 and the matrix is not unitary; statements using kC accordingly carry the hypotheses that force r \neq 0. The definitions are noncomputable, as are Real.sqrt and complex division.