Definitions/Def_CerednikDrinfeld_DescentIntertwiningBase.lean

DescentIntertwiningBase is a proposition asserting that two packages of data — on one side a rigid-analytic Mumford quotient, on the other an abstract tower of function fields over \overline{\mathbb Q} — are intertwined at the base level of the prime-to-qq' tower. Its context fixes natural numbers q,q',r and indices i_r,i_{\bar r}\in\{0,1\}; a valuation subring A of \overline{\mathbb Q} satisfying the predicate ValuationSubring.DecompositionIsometric over \mathbb Q, with completion C_A=A.valuation.Completion and distinguished subfield K_0=ValuationSubring.ratClosure A; a homomorphism \rho\colon\mathbb H[\mathbb Q,a,b]^\times\to\mathrm{PGL}_2(K_0); a pseudo-uniformiser \varpi (an element of K_0 whose valuation in C_A lies strictly between 0 and 1 and bounds every nonzero element of K_0 between v(\varpi)^N and v(\varpi)^{-N}), through which the ring HolRingOf ϖ ρ of functions on the Drinfeld upper half-plane over C_A that are holomorphic on each affinoid carries a \mathbb H^\times-action by Möbius precomposition, assumed to be a domain, with fraction field \mathcal M; level subgroups \Gamma_j indexed by the tower objects j (a base level none and one level for each prime \ell\neq q,q'); elements w_j,\bar w_j and s_\ell of the quaternion unit group; a homomorphism d from the decomposition group D_A to the valuation-preserving automorphisms of C_A fixing K_0 pointwise; and, on the other side, a field F_0/\overline{\mathbb Q}, tower data \mathbb T (curve function fields F_\ell with two finite integral degeneracy maps \varphi_{\ell,0},\varphi_{\ell,1}\colon F_0\to F_\ell), semilinear actions of D_A on F_0 and on each F_\ell, and semilinear automorphisms W_0,W_1 of F_0 with companions W_{\ell,0},W_{\ell,1}.

The data constrained are a character \chi\colon D_A\to\{\pm1\} (written multiplicatively in \mathrm{ZMod}\,2) and ring homomorphisms \iota_j from each tower field into \mathcal M. The conjunction asserts: \chi is trivial on the elements of D_A lying in A.inertiaSubgroupIn ℚ; \chi is non-trivial at every \varphi with A.IsFrobeniusAt for \varphi and r; \chi\tau=1 if and only if \tau fixes every x in the residue field of A with x^{r^2}=x; on \overline{\mathbb Q}-constants \iota_{\mathrm{none}} agrees with \overline{\mathbb Q}\to C_A\to\mathcal M; the subfield of \mathcal M generated by C_A together with \iota_{\mathrm{none}}(F_0) equals the field of \Gamma_{\mathrm{none}}-invariants Mumford.invariantFieldOf; \iota_{\mathrm{none}} sends finite \overline{\mathbb Q}-linearly independent families in F_0 to C_A-linearly independent families; for \tau\in D_A and x\in F_0, \iota_{\mathrm{none}}(\tau\cdot x) equals the semilinear twist of \iota_{\mathrm{none}}(x) by d(\tau) (via toAmbientOf and fracMap), multiplied by the action of 1 or of w_{\mathrm{none}} according as \chi\tau=1 or not; W_{i_r} and W_{i_{\bar r}} correspond to the actions of w_{\mathrm{none}} and \bar w_{\mathrm{none}}; and for each \ell the two degeneracy maps correspond to the identity and to the action of s_\ell on \iota_{\mathrm{none}}. The constant-field, Galois and Atkin–Lehner conditions are imposed at the base level only, the upper levels entering through the two degeneracy clauses.