Definitions/Def_CerednikDrinfeld_DescentIntertwining_v2.lean

CerednikDrinfeld.DescentIntertwining is one predicate on a whole package of data, asserting fourteen compatibilities between an abstract tower of function fields over \overline{\mathbb Q} and the field of meromorphic functions on a Drinfeld upper half-plane. The data are: a natural number r and two indices i_r,i_{\bar r}\in\{0,1\}; a valuation subring A of \overline{\mathbb Q} (with the DecompositionIsometric hypothesis registered), its completion A.valuation.Completion and the subfield ValuationSubring.ratClosure A inside it; a rational quaternion algebra \mathbb H[\mathbb Q,a,b] with a homomorphism \rho from its unit group to \mathrm{PGL}_2 of that subfield; a pseudo-uniformiser \varpi, i.e. an element of the subfield whose image has valuation strictly between 0 and 1 and such that every nonzero element of the subfield has valuation squeezed between v(\varpi)^{N} and v(\varpi)^{-N} for some N; the ring Omega.HolRingOf ϖ ρ of functions on the upper half-plane whose restriction to each affinoid affinoid ϖ n is a uniform limit of uniformly bounded pole-free rational functions, assumed to be a domain and carrying the quaternion units through \rho by Möbius precomposition; level subgroups \Gamma_j indexed by HeckeTower.Obj q q' (a base level together with one level per prime \ell\notin\{q,q'\}), elements w_j,\bar w_j per level and s_\ell per prime; a homomorphism dIso from the decomposition subgroup D_A to the valuation-preserving ring automorphisms of the completion fixing the subfield pointwise; on the other side a field F_0 over \overline{\mathbb Q} and a HeckeTower.TowerData \mathbb T (fields F_\ell that are curves over \overline{\mathbb Q}, each with two finite integral \overline{\mathbb Q}-algebra maps \varphi_{\ell,0},\varphi_{\ell,1} from F_0), semilinear D_A-actions gal₀ on F_0 and galT ℓ on F_\ell, two distinguished semilinear automorphisms W_0,W_1 of F_0 and W_{\ell,0},W_{\ell,1} of each F_\ell; finally a character \chi of D_A with values in the group of order two and ring homomorphisms \iota_j from the level-j field of the tower to \operatorname{Frac} of the holomorphic ring.

The asserted conjunction is: \chi is trivial on A.inertiaSubgroupIn ℚ; \chi(\varphi)\ne 1 for every \varphi with A.IsFrobeniusAt φ r; \chi(\tau)=1 exactly when \tau fixes every element x of the residue field of A with x^{r^2}=x; each \iota_j restricted to \overline{\mathbb Q} is the canonical map into the completion followed by the structure map; for each level the subfield generated by the constants (the image of the completion) and the image of \iota_j is exactly Mumford.invariantFieldOf for \Gamma_j, i.e. the subfield of elements fixed by every \gamma\in\Gamma_j; each \iota_j sends finite \overline{\mathbb Q}-linearly independent families to families linearly independent over the completion; for every \tau\in D_A and every x, \iota_j(\mathrm{gal}_\tau\cdot x) equals the image of \iota_j(x) under the semilinear automorphism of the fraction field induced by dIso τ, twisted by 1 or by w_j according as \chi(\tau)=1 or not (stated separately for the base level and for each \ell); \iota_j turns the semilinear automorphism with index i_r into multiplication by w_j and the one with index i_{\bar r} into \bar w_j, again level by level; and the two degeneracy maps satisfy \iota_{\ell}\circ\varphi_{\ell,0}=\iota_{0} and \iota_{\ell}\circ\varphi_{\ell,1}=s_\ell\cdot\iota_{0}. No characterising law of the parameters (\rho, \varpi, the \Gamma_j, w_j, s_\ell) is part of the predicate; these are pure compatibilities of the chosen maps.