Definitions/Def_ModularCurve_JOnePOps.lean

Over a fixed natural number p and a geometric datum G : NeronSpecialFibreGeom p — that is, abelian groups J^0_s, J_I, J_E, an additive subgroup T \subseteq J^0_s (the field torus), and a surjective additive map \pi \colon J^0_s \to J_I \times J_E whose kernel is exactly T — the module defines a structure ModularCurve.JOneP.NeronSpecialFibreOps G packaging operators on that datum together with the relations they are required to satisfy. The data fields are: families hecke, heckeI, heckeE of additive endomorphisms of J^0_s, J_I, J_E indexed by \mathbb{N}; two group homomorphisms diamondP and inertia from (\mathbb{Z}/p)^\times into the additive automorphism group of J^0_s; a family diamondN of additive endomorphisms of J^0_s indexed by \mathbb{N}; an additive automorphism w of J^0_s; additive endomorphisms verI of J_I and frobE of J_E; and a family diamondNI of additive endomorphisms of J_I.

The law fields are carried as hypotheses of the structure: the endomorphisms hecke ℓ commute with one another, and each commutes with every diamondP b and every inertia b; both diamondP b and inertia b fix every element of T; for \ell \neq p the projection is equivariant, \pi(T_\ell x) = (T_\ell \pi(x)_1, T_\ell \pi(x)_2) with the three hecke families at index \ell; and at \ell = p the Eichler–Shimura-shaped identity \pi(T_p x) = \bigl(\langle p\rangle\,V(\pi(x)_1),\, F(\pi(x)_2)\bigr) holds for all x \in J^0_s, where \langle p \rangle = diamondNI p, V = verI and F = frobE. No law constrains diamondN or w, which are pure data here; nothing is constructed or proved in the module, so an instance of the structure must supply all operators and all relations.