Definitions/Def_CerednikDrinfeld_EquivariantUniformization.lean

This module defines the structure CerednikDrinfeld.Mumford.EquivariantUniformization, parametrised by a prime r, a degeneracy datum D on a finite edge set E and a vertex set V (maps a,b\colon E\to V and widths w\colon E\to\mathbb{N}^{+}), a valuation subring A of \overline{\mathbb{Q}} with r a nonunit of A (LiesOverPrime), an abelian group T, a group S, and three homomorphisms out of S: a scalar part \mathrm{scalar}\colon S\to D_A into the decomposition group of A over \mathbb{Q}, an action \mathrm{actZ} of S by \mathbb{Z}-linear automorphisms of the ribbon kernel Z=\mathrm{ribbonKernel}\,D=\ker(\mathrm{pushforward}\,D.a)\cap\ker(\mathrm{pushforward}\,D.b)\subseteq(E\to\mathbb{Z}), and an action \mathrm{gal} of S on T by additive automorphisms. An instance of the structure consists of: an intermediate field K of \mathbb{Q} inside the completion C_A of A's valuation; an additive map \mathrm{ord}\colon \mathrm{Additive}\,K^{\times}\to\mathbb{Z} with v(k)=v(r)^{\mathrm{ord}(k)} for all k\in K^{\times}; the condition that every \sigma\in D_A lying in the inertia subgroup fixes K pointwise, read through any \mathbb{Q}-algebra automorphism s of C_A inducing the action of \sigma; a Henselian n-th root condition, namely that for n>0 with r\nmid n every k\in K^{\times} with \mathrm{ord}(k)=0 is an n-th power in K^{\times}; a period datum P over D with values in K, i.e. a symmetric \mathbb{Z}-bilinear Q\colon Z\times Z\to \mathrm{Additive}\,K^{\times} with \mathrm{ord}\,Q(x,y)=\sum_{e}w(e)x_ey_e; and a surjective additive map \mathrm{eFull} from the full torus points \mathrm{Hom}_{\mathbb{Z}}(Z,\mathrm{Additive}\,C_A^{\times}) onto T whose kernel is exactly the period lattice, the image of Q after base change to C_A.

Two equivariance fields carry the symmetry. For \sigma\in S and any \mathbb{Q}-algebra automorphism s of C_A realising the action of \mathrm{scalar}(\sigma): first s(Q(x,y))=Q(\mathrm{actZ}(\sigma)x,\mathrm{actZ}(\sigma)y) in C_A, and second \mathrm{eFull}\bigl(s\circ u\circ \mathrm{actZ}(\sigma)^{-1}\bigr)=\mathrm{gal}(\sigma)\,\mathrm{eFull}(u), where the postcomposition with s on coefficients is coeffMap and the precomposition with \mathrm{actZ}(\sigma)^{-1} is precomp. Thus the structure asserts an S-equivariant presentation of T as the quotient of the full character torus points by the period lattice, rather than the torsion-level, Hecke-compatible statement recorded by PeriodUniformization in the companion module; no compatibility with Hecke correspondences is imposed here.