Definitions/Def_ModularCurve_LaurentBaseChangeTower.lean

Throughout, L is a field with a \mathbb{Q}-algebra structure and F_0 is an intermediate field of L((q))'s rational model, namely of the extension \mathbb{Q}((q))/\mathbb{Q}; laurentBaseChange L F₀ denotes the intermediate field of L((q))/L generated by the image of F_0 under the coefficientwise ring homomorphism coeffEmb L, which applies \mathbb{Q} \to L to each Laurent coefficient. The module equips this base-changed field with the structure maps making it sit at the top of two towers.

baseChangeRingHom is the ring homomorphism F_0 \to L\cdot F_0 sending y to the element \mathrm{coeffEmb}_L(y) of L((q)) together with the proof that it lies in laurentBaseChange L F₀; coe_baseChangeRingHom records that its underlying Laurent series is exactly \mathrm{coeffEmb}_L(y). baseChangeAlgebra is the F_0-algebra structure on L\cdot F_0 obtained from this homomorphism, and algebraMap_laurentBaseChange_eq identifies the resulting structure map with baseChangeRingHom. baseChangeAlgebraRat is the \mathbb{Q}-algebra structure on L\cdot F_0 obtained from the composite \mathbb{Q} \to L \to L\cdot F_0 of the given \mathbb{Q}-algebra map of L with the inclusion of L into the intermediate field. Both algebra structures are reducible definitions rather than global instances. The two remaining declarations are instances asserting that the scalar actions compose correctly: with the \mathbb{Q}- and F_0-actions on L\cdot F_0 taken to be precisely those coming from the two definitions above, \mathbb{Q} \subseteq L \subseteq L\cdot F_0 and \mathbb{Q} \subseteq F_0 \subseteq L\cdot F_0 are scalar towers; the actions involved are written out explicitly in the statements so that they refer to these structures and not to any other rational action available on a subfield.