Definitions/Def_ModularCurve_DRModelPackageLevelCrossingFrame.lean

Throughout, q is a prime, N_0\ge 1 with q\nmid N_0, and \mathfrak X is a DRModelPackageLevel N₀ q hqN, whose underlying scheme is DRLevel.X N₀ q = IgusaScheme (N₀*q) q with its structure morphism to \operatorname{Spec} of R_q= DRLevel.R q; further data are a ring map \rho_O\colon R_q\to O and a ring map \mathrm{to}\kappa\colon O\to\kappa into an algebraically closed field \kappa of characteristic q. Here X_O= DRLevel.XO ρO is the base change X\times_{\operatorname{Spec}R_q}\operatorname{Spec}O, and DRLevel.bcMap ρO toκ is the induced morphism from the geometric fibre DRLevel.fibre (toκ ∘ ρO) to X_O.

Five abbreviations are introduced. DRLevel.XO.toBase ρO names the second pullback projection X_O\to\operatorname{Spec}(O). For a point n of the fibre product of the two component morphisms \mathfrak X.\mathrm{comp}\,\kappa\,(\mathrm{to}\kappa\circ\rho_O)\,0 and \dots\,1 (each a closed immersion of the level-N_0 geometric fibre fibre0 into the level-N_0q geometric fibre), crossingPt is the image of n in the topological space of X_O under the first projection, followed by the component indexed 0, followed by bcMap ρO toκ. baseGerm ρO x o, for x\in X_O and o\in O, is the germ at x of the global section of X_O obtained by transporting o to a global section of \operatorname{Spec}(O) and pulling it back along the structure morphism; it lies in the stalk \mathcal O_{X_O,x}. Finally ξinf and ξzero are the images in X_O of the generic point of fibre0 — integral by DRModelPackageLevel.isIntegral_fibre0 — under the component indexed 0, respectively 1, followed by bcMap ρO toκ; thus they are the generic points of the images of the two components of the q-fibre. Nothing is asserted here: the module only fixes notation.