Definitions/Def_ModularCurve_JLinePlacesBar.lean

Fix a level N \ge 1. The modular function field of level N over \overline{\mathbb Q} is here modularFunctionFieldBar N, the subfield of \overline{\mathbb Q}((q)) generated over \overline{\mathbb Q} by the coefficientwise images (under coeffEmb, i.e. application of \mathbb Q \to \overline{\mathbb Q} to each Laurent coefficient) of the field modularFunctionFieldFull N, which is the \mathbb Q-subfield of \mathbb Q((q)) generated by the series q-expansions \mathrm{jq} rescaled by q \mapsto q^{d} for all divisors d \mid N. Write \bar j for the element of that field given by the coefficientwise image of the q-expansion \mathrm{jq} of the modular invariant, with membership supplied by jq_mem_full. The abbreviation jLineBar N is the intermediate field \overline{\mathbb Q}(\bar j), i.e. the \overline{\mathbb Q}-subfield of modularFunctionFieldBar N generated by \bar j, together with its \overline{\mathbb Q}-algebra and \overline{\mathbb Q}-module structures; transcendental_jLineBar_gen records that \bar j is transcendental over \overline{\mathbb Q}, quoting transcendental_coeffEmb_jq. Consequently jLineBarRingEquiv N is a ring isomorphism \overline{\mathbb Q}(T) \cong \overline{\mathbb Q}(\bar j), namely the underlying ring map of Mathlib's algebra isomorphism attached to a transcendental element; accompanying lemmas state that it acts as the identity on constants from \overline{\mathbb Q} and sends T to \bar j.

Three places of \overline{\mathbb Q}(\bar j) over \overline{\mathbb Q} are then fixed. A Place K F is a valuation subring of F containing the image of K, proper in F, and a principal ideal ring; Place.congrRingEquiv transports a place along a ring isomorphism compatible with the structure maps by pulling the valuation subring back along the inverse isomorphism. Applying this to jLineBarRingEquiv N gives jLineBarPlace1728 N, jLineBarPlaceZero N and jLineBarPlaceInfty N, the transports of the places of \overline{\mathbb Q}(T) cut out by the primes (T - 1728) and (T) of \overline{\mathbb Q}[T] and of the place at infinity given by the degree valuation. A classical decidable-equality helper for \overline{\mathbb Q}(T) accompanies the last of these.