Definitions/Def_AutomorphicForm_ProductionPinsCompact.lean

For a number field F this module defines productionPinsCompact F : CarrierPins F, a package of the data on which the project's automorphy predicates are evaluated. CarrierPins F is a structure bundling a measurable space mS and a measure μ on \mathrm{GL}_2(\mathbb{A}_F), a set D in that group, a subgroup Z of the idele units, a map U from ideals of \mathcal{O}_F to subgroups of \mathrm{GL}_2(\mathbb{A}_F), a map gen from finite places to group elements, and a measurable space nS with a measure ν on \mathbb{A}_F. The instance is obtained from productionPinsOf, so mS and nS are the Borel structures, μ is the Haar measure adelicGLHaar, Z is the full group \top, and ν is the additive Haar measure on \mathbb{A}_F conditioned (via ProbabilityTheory.cond) on the fundamental box adelicBox F; the chosen slots are D the centre-cut Siegel set with parameters (1/2,1,1/2,2), gen v the Hecke element \mathrm{diag}(\pi_v,1) at v and 1 elsewhere, and U N = levelOne (𝓞 F) F N ⊓ finiteAdelicGL2Subgroup F. Since levelOne N constrains only the finite component — the finite part of g and of g^{-1} must have integral entries, lower-left entry in the N-ball and lower-right entry congruent to 1 — it contains the whole archimedean factor; intersecting with finiteAdelicGL2Subgroup F, the kernel of the archimedean projection glArch, cuts this out, leaving exactly the elements with archimedean part 1 and finite part in finiteLevelOne N. This is the only slot in which productionPinsCompact F differs from productionPins F. The accompanying lemmas record the eight slot values by rfl, the two membership consequences (\mathrm{glFin}\,u \in finiteLevelOne N, \mathrm{glArch}\,u = 1), the identity U N = (productionPins F).U N ⊓ finiteAdelicGL2Subgroup F with the resulting inclusion, and the transfer of the measure-theoretic facts: μ is Haar, ν is a probability measure, D is measurable and 0 < \mu(D) < \infty.