Definitions/Def_ModularCurve_RouteBCoordRing.lean

Fix N\ge 1 (nonzero) and recall that modularFunctionField N is the intermediate field \mathbb Q\bigl(j(q),\,j(q^N)\bigr) of \mathbb Q(\!(q)\!), obtained by adjoining to \mathbb Q the Laurent series jq and its N-fold q-substitution qExpand ℚ N jq. Three things are defined here. First, jAdjoinRingHom N is the ring homomorphism \mathbb Q(j(q))\to\mathbb Q(j(q),j(q^N)) realising the inclusion of the simple extension \mathbb Q\langlejq\rangle into modularFunctionField N provided by adjoin_jq_le; on underlying Laurent series it is the identity. Second, algebraIntPolyModularFunctionField N is the \mathbb Z[X]-algebra structure on modularFunctionField N whose structure map is evalAtJGen (evaluation of integer polynomials at jGen, the element jq of \mathbb Q\langlejq\rangle) followed by that inclusion; thus X\mapsto j(q), and the polynomial ring \mathbb Z[X] acts as \mathbb Z[j], the coordinate ring of the affine j-line over \mathbb Z. Third, with this structure in force, routeBCoordRing N is the integral closure of \mathbb Z[X] in modularFunctionField N, i.e. the subalgebra of those elements of \mathbb Q(j(q),j(q^N)) that are integral over \mathbb Z[j] — the normalisation of the j-line in the function field, the affine coordinate ring of the intended integral model of Y_0(N). Finally, for a commutative ring L and a ring homomorphism \varphi from routeBCoordRing N to L, routeBJValue φ is the element \varphi(j(q))\in L, the image under \varphi of the distinguished coordinate coming from X\in\mathbb Z[X]; this is the j-invariant attached to the L-point \varphi.