Definitions/Def_CerednikDrinfeld_JPrimeTorsionDatum.lean

For a natural number p, finite types E, V and a valuation subring A of \overline{\mathbb{Q}}, CerednikDrinfeld.JPrimeTorsionDatum p E V A is a structure bundling the combinatorial and arithmetic data by which the p-torsion of a Jacobian with purely toric reduction is handled. Its fields are: a DegeneracyData E V, i.e. two maps a,b : E \to V and widths w : E \to \mathbb{N}_{>0}; a HeckeData on it, i.e. commuting integer matrices T_\ell on \mathbb{Z}^E and T_{v,\ell} on \mathbb{Z}^V indexed by the primes, a finite exceptional set S outside which T_\ell intertwines the two degeneracy pushforwards \mathbb{Z}^E \to \mathbb{Z}^V with T_{v,\ell}, and stability of the joint kernel of these pushforwards under every T_\ell; a type T that is a finite abelian group, together with the requirement p\,t = 0 for all t \in T; a ring homomorphism from HeckeAlg = \mathbb{Z}[X_\ell : \ell \text{ prime}] to \mathrm{End}_{\mathbb{Z}}(T); a homomorphism \mathrm{gal} from the group of \mathbb{Q}-algebra automorphisms of \overline{\mathbb{Q}} to the additive automorphisms of T, commuting with the Hecke action elementwise; the condition that \mathrm{gal} be trivial on the automorphisms fixing pointwise some intermediate field L with \mathbb{Q} \subseteq L \subseteq \overline{\mathbb{Q}} finite over \mathbb{Q}; a subgroup \mathrm{toric} \le T together with an isomorphism of it onto the group of \mathbb{Z}-linear maps \mathrm{ribbonKernel}\,D \to \mathbb{Z}/p; and an additive map \mathrm{sp} from the subgroup of elements fixed by every \sigma in the inertia subgroup of A over \mathbb{Q} (the intersection over such \sigma of the kernels of \mathrm{gal}\,\sigma - \mathrm{id}) to \mathrm{ribbonComponentGroup}\,D, the quotient of \mathrm{Hom}_{\mathbb{Z}}(\mathrm{ribbonKernel}\,D, \mathbb{Z}) by the image of the Gram map of the width pairing \sum_e w_e x_e y_e. No property relating these data is asserted beyond the listed fields. Two subgroups of T are then named: invariants, the inertia invariants at A just described, and W Dm 𝔪, the intersection over x \in \mathfrak{m} of the kernels of \mathrm{hecke}\,x, i.e. the \mathfrak{m}-torsion of T for an ideal \mathfrak{m} of HeckeAlg.